strictMono_add_left_of_ne_top — Mathlib

English

If b ≠ ⊤, the map x ↦ x + b is strictly increasing: x < y implies x + b < y + b.

Русский

Если b ≠ ⊤, отображение x ↦ x + b строго возрастает: x < y ⇒ x + b < y + b.

LaTeX

$$b \neq \top \Rightarrow \text{StrictMono}(\lambda x. x + b)$$

Lean4

theorem strictMono_add_left_of_ne_top (b : α) (h : b ≠ ⊤) : StrictMono (fun x ↦ x + b) :=
  by
  apply Monotone.strictMono_of_injective
  · apply Monotone.add_const monotone_id
  · apply injective_add_left_of_ne_top _ h

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