add_lt_add_left — Mathlib

English

If x ≠ ⊥ in WithBot α and y < z, then x + y < x + z, assuming LT α and AddLeftStrictMono α.

Русский

Если x ≠ ⊥ в WithBot α и y < z, то x + y < x + z, при условии LT α и AddLeftStrictMono α.

LaTeX

$$$$\\forall x,y,z \\in \\mathrm{WithBot}(\\alpha),\\ x \\neq \\bot \\;\\Rightarrow\\; (y

Lean4

protected theorem add_lt_add_left [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) : y < z → x + y < x + z := by
  lift x to α using hx; cases y <;> cases z <;> simp [← coe_add]; simpa using (add_lt_add_left · _)

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