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.

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