inv_hom_apply — Mathlib

English

If e is an isomorphism M ≅ N in CommMonCat, then applying the inverse after the forward map yields the original element: e.inv (e.hom x) = x for all x ∈ M.

Русский

Если e — изоморфизм M ≅ N в CommMonCat, то применение обратного после прямого отображает исходный элемент: e.inv (e.hom x) = x для всех x ∈ M.

LaTeX

$$$\forall x:\; e^{-1}(e(x)) = x,$ где $e: M \cong N$.$$

Lean4

@[to_additive]
theorem inv_hom_apply {M N : CommMonCat} (e : M ≅ N) (x : M) : e.inv (e.hom x) = x := by simp

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