add_lt_add_right_coe — Mathlib

English

If x < y in EReal, then for every real z, x + z < y + z.

Русский

Если x < y в EReal, то для каждого вещественного z выполняется x+z < y+z.

LaTeX

$$$\\\\forall {x,y \\\\in \\\\mathrm{EReal}} \\\\ x < y \\\\Rightarrow \\\\forall z \\\\in \\\\mathbb{R}, \\\\ x + z < y + z$$$

Lean4

theorem add_lt_add_right_coe {x y : EReal} (h : x < y) (z : ℝ) : x + z < y + z :=
  not_le.1 <| mt (addLECancellable_coe z).add_le_add_iff_right.1 h.not_ge

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