add_lt_add_of_lt_of_le — Mathlib

English

If x < y and z ≤ t with z ≠ ⊥ and t ≠ ⊤, then x + z < y + t.

Русский

Если x < y и z ≤ t, причём z ≠ ⊥ и t ≠ ⊤, то x + z < y + t.

LaTeX

$$$\\\\forall {x y z t \\\\in \\\\mathrm{EReal}},\\\\ x < y \\\\land z \\le t \\\\land z \\\\ne \\bot \\\\land t \\\\ne \\top \\\\Rightarrow x + z < y + t$$$

Lean4

/-- See also `EReal.add_lt_add_of_lt_of_le'` for a version with weaker but less convenient
assumptions. -/
theorem add_lt_add_of_lt_of_le {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hz : z ≠ ⊥) (ht : t ≠ ⊤) : x + z < y + t :=
  add_lt_add_of_lt_of_le' h h' (ne_bot_of_le_ne_bot hz h') fun ht' => (ht ht').elim

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