add_lt_add_of_lt_of_le — Mathlib

English

Let α be a preorder with AddLeftMono and AddRightStrictMono. If x ≠ ⊤, w < y, and x ≤ z, then w + x < y + z.

Русский

Пусть α — множество с предельным порядком, добавление слева монотонно, добавление справа строго монотонно. Если x ≠ ⊤, w < y, и x ≤ z, то w + x < y + z.

LaTeX

$$$\\\\forall {\\\\alpha} [Preorder \\\\alpha] [AddLeftMono \\\\alpha] [AddRightStrictMono \\\\alpha] {\\\\,w \\\\,x \\\\,y \\\\,z : WithTop \\\\alpha}, \\\\ (x \\\\neq \\\\top) \\\\to (w < y) \\\\to (x \\\\le z) \\\\to 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 :=
  (WithTop.add_lt_add_right hx hwy).trans_le <| add_le_add_left hxz _

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