finsuppUnique_symm_apply — Mathlib

English

The inverse of the finsuppUnique map sends an element m ∈ M to the singleton function with value m at the unique index.

Русский

Обратное отображение finsuppUnique отправляет элемент m∈M в синглтон-функцию, значение которой равно m в уникальном индексе.

LaTeX

$$$(LinearEquiv.finsuppUnique R M α)^{-1} (m) = \text{single default } m$$$

Lean4

@[simp]
theorem finsuppUnique_symm_apply (m : M) : (LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m := by
  ext; simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single, equivFunOnFinite, Function.update]

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