hom_inv_apply — Mathlib

English

Let X and Y be bounded orders and e an isomorphism X ≅ Y. Then the forward map composed with the inverse equals the identity on Y; equivalently, for every s in Y, e.hom(e.inv(s)) = s.

Русский

Пусть X и Y — ограниченные порядки, e — изоморфизм X ≅ Y. Тогда композиция перехода вперёд с обратным сопоставлением является тождественной на Y; то есть для каждого s ∈ Y выполняется e.hom(e.inv(s)) = s.

LaTeX

$$$e.hom \circ e.inv = \mathrm{id}_Y$$$

Lean4

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

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