fintype instances for sigma types #
instance
instFintypeSigma
{α : Type u_1}
(β : α → Type u_2)
[inst : Fintype α]
[inst : (a : α) → Fintype (β a)]
:
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_1}
{β : α → Type u_2}
[inst : Fintype α]
[inst : (a : α) → Fintype (β a)]
:
(Finset.sigma Finset.univ fun a => Finset.univ) = Finset.univ
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))