toEquivRange_symm_apply_self — Mathlib

English

The inverse of toEquivRange sends back the original element: f.toEquivRange.symm (⟨f(a), mem⟩) = a.

Русский

Обратная к toEquivRange возвращает исходный элемент: f.toEquivRange.symm(⟨f(a), mem⟩) = a.

LaTeX

$$$f.toEquivRange^{-1}\\langle f(a), \\mathrm{mem\\_range\\_self}(a) \\rangle = a$$$

Lean4

@[simp]
theorem toEquivRange_symm_apply_self (a : α) : f.toEquivRange.symm ⟨f a, Set.mem_range_self a⟩ = a := by
  simp [Equiv.symm_apply_eq]

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