apply_eq_iff_eq_symm_apply — Mathlib

English

Let e be an order isomorphism between two preordered sets. Then for all x in α and y in β we have e(x) = y if and only if x = e^{-1}(y).

Русский

Пусть e — упорядоченная изоморфия между упорядоченными множествами. Тогда для любых x ∈ α и y ∈ β верно: e(x) = y тогда и только если x = e^{-1}(y).

LaTeX

$$$ e x = y \iff x = e^{-1} y $$$

Lean4

theorem apply_eq_iff_eq_symm_apply (e : α ≃o β) (x : α) (y : β) : e x = y ↔ x = e.symm y :=
  e.toEquiv.apply_eq_iff_eq_symm_apply

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