mathlib3 documentation

data.fintype.sigma

fintype instances for sigma types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def sigma.fintype {α : Type u_1} (β : α Type u_2) [fintype α] [Π (a : α), fintype (β a)] :
Equations
@[simp]
theorem finset.univ_sigma_univ {α : Type u_1} {β : α Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
@[protected, instance]
def psigma.fintype {α : Type u_1} {β : α Type u_2} [fintype α] [Π (a : α), fintype (β a)] :
fintype (Σ' (a : α), β a)
Equations