equivFunOnFinite_symm_coe — Mathlib

English

If α has a unique element, the type of finitely supported functions α →₀ M is equivalent to M; evaluation at that unique element gives the bijection.

Русский

Если у α есть единственный элемент, множество функций с конечной опорой α →₀ M эквивалентно M; отображение по единственному элементу образует биекцию.

LaTeX

$$Equiv (Finsupp α M) M \\text{ for } [Unique α]$$

Lean4

@[simp]
theorem equivFunOnFinite_symm_coe {α} [Finite α] (f : α →₀ M) : equivFunOnFinite.symm f = f :=
  equivFunOnFinite.symm_apply_apply f

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