inv_hom_apply — Mathlib

English

Let e be an isomorphism X ≅ Y in CommGrpCat and x ∈ X. Then e.inv (e.hom x) = x.

Русский

Пусть e — изоморфизм X ≅ Y в CommGrpCat и x ∈ X. Тогда e.inv (e.hom x) = x.

LaTeX

$$$$ \forall X,Y\, (e : X \cong Y),\ \forall x \in X,\ e.inv (e.hom x) = x. $$$$

Lean4

@[to_additive]
theorem inv_hom_apply {X Y : CommGrpCat} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x := by
  simp
    -- This is essentially an alias for `Iso.inv_hom_id_apply`; consider deprecation?

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