equivFunOnFintype_symm_single — Mathlib

English

For a finite index type, the inverse of the equivalence applied to a pure Pi.single is the corresponding singleton.

Русский

Для конечного типа индексов обратная к эквиваленции, примененная к Pi.single, равна соответствующему одиночному элементу.

LaTeX

$$$(\mathrm{equivFunOnFintype})^{-1}(\Pi\text{single } i m) = \mathrm{single}\ i\ m$$$

Lean4

@[simp]
theorem equivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : β i) :
    (@DFinsupp.equivFunOnFintype ι β _ _).symm (Pi.single i m) = DFinsupp.single i m :=
  by
  ext i'
  simp only [← single_eq_pi_single, equivFunOnFintype_symm_coe]

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