fintype instances for sigma types

instance instFintypeSigma {α : Type u_4} (β : α → Type u_5) [Fintype α] [(a : α) → Fintype (β a)] : Fintype (Sigma β)

Equations

• instFintypeSigma β = { elems := Finset.sigma Finset.univ fun (x : α) => Finset.univ, complete := (_ : ∀ (x : Sigma β), x ∈ Finset.sigma Finset.univ fun (x : α) => Finset.univ) }

@[simp]

theorem Finset.univ_sigma_univ {α : Type u_4} {β : α → Type u_5} [Fintype α] [(a : α) → Fintype (β a)] : (Finset.sigma Finset.univ fun (a : α) => Finset.univ) = Finset.univ

instance PSigma.fintype {α : Type u_4} {β : α → Type u_5} [Fintype α] [(a : α) → Fintype (β a)] : Fintype ((a : α) ×' β a)

Equations

• PSigma.fintype = Fintype.ofEquiv ((i : α) × β i) (Equiv.psigmaEquivSigma fun (a : α) => β a).symm