inv_hom_apply — Mathlib

English

Let e be an isomorphism between SemiNormedGrp₁ objects M and N. Then applying the inverse map to the image of any element of M returns the original element; equivalently, e^{-1} ∘ e = id_M (so e^{-1}(e(r)) = r for all r ∈ M).

Русский

Пусть e — изоморфизм между объектами SemiNormedGrp₁ M и N. Тогда применение обратного отображения к образу любого элемента M возвращает исходный элемент; эквивалентно e^{-1} ∘ e = id_M (для всякого r ∈ M выполняется e^{-1}(e(r)) = r).

LaTeX

$$$\\forall r\\in M:\\ e^{-1}(e(r)) = r$$$

Lean4

@[simp]
theorem inv_hom_apply {M N : SemiNormedGrp₁} (e : M ≅ N) (r : M) : e.inv (e.hom r) = r :=
  by
  rw [← comp_apply]
  simp

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