add_lt_add_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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