right_inv_of_invOfMemRange — Mathlib

English

For every a ∈ α, invOfMemRange(⟨f(a), mem_range_self a⟩) = a; i.e., the inverse on the canonical image element returns the original a.

Русский

Для каждого a ∈ α invOfMemRange(⟨f(a), mem_range_self a⟩) = a; то есть обратное отображение на элементе образа возвращает исходный a.

LaTeX

$$$\\forall a:\\, invOfMemRange(\\langle f(a), \\mathrm{mem\\_range\\_self}(a)\\rangle) = a$$$

Lean4

@[simp]
theorem right_inv_of_invOfMemRange (a : α) : f.invOfMemRange ⟨f a, Set.mem_range_self a⟩ = a :=
  f.injective.right_inv_of_invOfMemRange a

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