map_inv_le_map_inv_iff — Mathlib

English

For an order-isomorphism f, the inverse map preserves and reflects order in a precise way: EquivLike.inv f b ≤ EquivLike.inv f a iff b ≤ a.

Русский

Для отображения-изоморфизма f обратное отображение сохраняет и отражает порядок так: EquivLike.inv f b ≤ EquivLike.inv f a ⇔ b ≤ a.

LaTeX

$$$\forall {f:\ F} {a,b},\ EquivLike.inv f b \le EquivLike.inv f a \iff b \le a$$$

Lean4

theorem map_inv_le_map_inv_iff (f : F) {a b : β} : EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a := by simp

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