Documentation

Mathlib.Data.Fintype.Sigma

fintype instances for sigma types #

instance instFintypeSigma {α : Type u_4} (β : αType u_5) [Fintype α] [(a : α) → Fintype (β a)] :
Equations
@[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