equivFunOnFintype_single — Mathlib

English

If ι is finite, there is an equivalence between DFinsupp β and ∀ i, β i.

Русский

Если ι конечен, существует эквиваленция между DFinsupp β и ∀ i, β i.

LaTeX

$$$\mathrm{DFinsupp}\, \beta \;\cong\; \prod_{i \in ι} β(i) \quad \text{при } [Fintype\ ι]$$$

Lean4

@[simp]
theorem equivFunOnFintype_single [Fintype ι] (i : ι) (m : β i) :
    (@DFinsupp.equivFunOnFintype ι β _ _) (DFinsupp.single i m) = Pi.single i m :=
  rfl

Похожие утверждения