inv_hom_apply — Mathlib

English

For any isomorphism e: X ≅ Y and any x ∈ X, applying the inverse after the forward map yields x: e.inv (e.hom x) = x.

Русский

Для изоморфизма e: X ≅ Y и любого x ∈ X выполнение обратного после прямого отображения возвращает x: e.inv (e.hom x) = x.

LaTeX

$$theorem inv_hom_apply {X Y : BddOrd} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x$$

Lean4

theorem inv_hom_apply {X Y : BddOrd} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x := by simp

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