le_iff — Mathlib

English

If f is left order continuous and injective, then f x ≤ f y iff x ≤ y.

Русский

Если f слева непрерывна и инъективна, то f x ≤ f y эквивално x ≤ y.

LaTeX

$$$\text{LeftOrdContinuous}(f) \wedge \text{Injective}(f) \Rightarrow (f x \le f y \Leftrightarrow x \le y)$$$

Lean4

theorem le_iff (hf : LeftOrdContinuous f) (h : Injective f) {x y} : f x ≤ f y ↔ x ≤ y := by
  simp only [← sup_eq_right, ← hf.map_sup, h.eq_iff]

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