equivFunOnFinite_symm_single — Mathlib

English

For DecidableEq α and Finite α, the symmetrized equivalence gives that the symmetric image of a Pi-single equals the corresponding finsupp singleton.

Русский

Для конечного множества α с допустимым равенством элементов эквивалентности симметрично отображает Pi.single в соответствующий finsupp singleton.

LaTeX

$$$\mathrm{equivFunOnFinite}.\mathrm{symm}(\Pi\.single(x,m)) = \mathrm{singleton}(x,m)$$$

Lean4

@[simp]
theorem equivFunOnFinite_symm_single [DecidableEq α] [Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite.symm (Pi.single x m) = Finsupp.single x m := by
  rw [← equivFunOnFinite_single, Equiv.symm_apply_apply]

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