add_lt_add_of_lt_of_le — Mathlib

English

If w ≠ ⊥, 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 < y \\;\\land\\; x \\le z \\Rightarrow w+x < y+z.$$$$

Lean4

protected theorem add_lt_add_of_lt_of_le [Preorder α] [AddLeftMono α] [AddRightStrictMono α] (hx : x ≠ ⊥) (hwy : w < y)
    (hxz : x ≤ z) : w + x < y + z :=
  (WithBot.add_lt_add_right hx hwy).trans_le <| add_le_add_left hxz _

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