symm_apply_lt — Mathlib

English

Let e be an order isomorphism between preordered types α and β. Then for every x in α and y in β, e.symm y < x if and only if y < e x.

Русский

Пусть e задаёт порядковый изоморфизм между типами α и β с предуровнями. Тогда для каждого x ∈ α и y ∈ β верно: e.symm(y) < x тогда и только если y < e(x).

LaTeX

$$$\forall x:\alpha\,\forall y:\beta\, e^{-1}(y) < x \iff y < e(x)$$$

Lean4

theorem symm_apply_lt (e : α ≃o β) {x : α} {y : β} : e.symm y < x ↔ y < e x := by rw [← e.lt_iff_lt, e.apply_symm_apply]

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