add_lt_add_of_le_of_lt — Mathlib

English

If w ≠ ⊥ and w ≤ y and x < z, then w + x < y + z, given Preorder α, AddLeftStrictMono α, AddRightMono α.

Русский

Если w ≠ ⊥ и w ≤ y и x < z, то w + x < y + z, при условии Preorder α, AddLeftStrictMono α, AddRightMono α.

LaTeX

$$$$\\forall w,x,y,z \\in \\mathrm{WithBot}(\\alpha),\\ w \\neq \\bot \\;\\land\\; w \\le y \\;\\land\\; x < z \\Rightarrow w+x < y+z.$$$$

Lean4

protected theorem add_lt_add_of_le_of_lt [Preorder α] [AddLeftStrictMono α] [AddRightMono α] (hw : w ≠ ⊥) (hwy : w ≤ y)
    (hxz : x < z) : w + x < y + z :=
  (WithBot.add_lt_add_left hw hxz).trans_le <| add_le_add_right hwy _

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