add_lt_add_left_coe

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.add_lt_add_left_coe

English

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

Русский

Если x < y в EReal, то для любого вещественного z верно z + x < z + y.

LaTeX

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

Lean4

theorem add_lt_add_left_coe {x y : EReal} (h : x < y) (z : ℝ) : (z : EReal) + x < z + y := by
  simpa [add_comm] using add_lt_add_right_coe h z

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru