hom_inv_apply — Mathlib · SciLib

English

Let e be an isomorphism M ≅ N. Then composing the inverse with the forward map on an element of N yields the identity: e.hom(e^{-1}(s)) = s for all s ∈ N; equivalently e ∘ e^{-1} = id_N.

Русский

Пусть e — изоморфизм M ≅ N. Тогда композиция обратноc опорного отображения с прямым отображением на элементе N даёт тождественный отображение: e(hom(e^{-1}(s))) = s для всех s ∈ N; эквивалентно e ∘ e^{-1} = id_N.

LaTeX

$$$\\forall s\\in N:\\ e(hom(e^{-1}(s))) = s$$$

Lean4

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

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