monotone_lt — Mathlib

English

For a fixed x in a preorder α, the map y ↦ x < y is monotone in y with respect to the order on α. Equivalently, for all y,z ∈ α, y ≤ z implies x < y implies x < z.

Русский

Для фиксированного x в предпорядке α отображение y ↦ x < y монотонно по y: если y ≤ z, то x < y следует x < z.

LaTeX

$$$\\\\forall y,z\\\\in \\\\alpha,\\\\ y \\\\le z \\\\Rightarrow x < y \\\\Rightarrow x < z$$$

Lean4

theorem monotone_lt {x : α} : Monotone (x < ·) := fun _ _ h' h => h.trans_le h'

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