injective_of_le_imp_le — Mathlib

English

If ∀ {x y}, f x ≤ f y → x ≤ y, then f is injective.

Русский

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

LaTeX

$$[PartialOrder α] [Preorder β] (f : α → β) (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f$$

Lean4

theorem injective_of_le_imp_le [PartialOrder α] [Preorder β] (f : α → β) (h : ∀ {x y}, f x ≤ f y → x ≤ y) :
    Injective f := fun _ _ hxy ↦ (h hxy.le).antisymm (h hxy.ge)

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