inv_hom_apply — Mathlib

English

If e: X ≅ Y is an isomorphism in the distributive lattice setting, then e.inv ∘ e.hom = id_X, i.e., the inverse map composed with the forward map is the identity on X.

Русский

Пусть e: X ≅ Y — изоморфизм в контексте ограниченных распределительных решёток. Тогда e.inv ∘ e.hom = id_X, то есть обратная карта, применённая после прямой, даёт тождество на X.

LaTeX

$$$ e^{-1} \circ e = \mathrm{id}_X $$$

Lean4

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

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