fintype instances for sigma types

ink

instance instFintypeSigma {α : Type u_1} (β : α → Type u_2) [inst : Fintype α] [inst : (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) }

ink

@[simp]

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

ink

instance PSigma.fintype {α : Type u_1} {β : α → Type u_2} [inst : Fintype α] [inst : (a : α) → Fintype (β a)] : Fintype ((a : α) ×' β a)

Equations

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