English
If ι is finite, there is an equivalence between the type of finitely supported families (Π₀ i, β i) and the full product ∀ i, β i.
Русский
Если ι конечен, существует эквивалентность между типом конечно-поддерживаемых семейств (Π₀ i, β i) и полным произведением ∀ i, β i.
LaTeX
$$$(\Pi₀ i, β i) \cong \prod_{i \in ι} β i \quad \text{when } [Fintype\ ι]$$$
Lean4
/-- Given `Fintype ι`, `equivFunOnFintype` is the `Equiv` between `Π₀ i, β i` and `Π i, β i`.
(All dependent functions on a finite type are finitely supported.) -/
@[simps apply]
def equivFunOnFintype [Fintype ι] : (Π₀ i, β i) ≃ ∀ i, β i
where
toFun := (⇑)
invFun f := ⟨f, Trunc.mk ⟨Finset.univ.1, fun _ => Or.inl <| Finset.mem_univ_val _⟩⟩
left_inv _ := DFunLike.coe_injective rfl
