coe_funUnique_symm — Mathlib

English

The inverse map of the canonical evaluation is the constant map: for each m ∈ M, the inverse sends m to the constant function ι → M with value m.

Русский

Обратная к каноническому отображению на значения — константное отображение: для каждого m ∈ M обратное отображение отправляет m в константную функцию ι → M, принимающую значение m.

LaTeX

$$$ (\mathrm{funUnique}_{ι,R,M})^{-1}(m) = \lambda i.\; m \quad \text{для всех } m \in M $$$

Lean4

@[simp]
theorem coe_funUnique_symm : ⇑(funUnique ι R M).symm = Function.const ι :=
  rfl

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