add_lt_add — Mathlib

English

If x < y and z < t in EReal, then x + z < y + t.

Русский

Если x < y и z < t в EReal, тогда x + z < y + t.

LaTeX

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

Lean4

theorem add_lt_add {x y z t : EReal} (h1 : x < y) (h2 : z < t) : x + z < y + t :=
  by
  rcases eq_or_ne x ⊥ with (rfl | hx)
  · simp [h1, bot_le.trans_lt h2]
  · lift x to ℝ using ⟨h1.ne_top, hx⟩
    calc
      (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
      _ ≤ y + t := add_le_add_right h1.le _

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