add_lt_top

Mathlib.Data.EReal.Operations

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

English

If x ≠ ⊤ and y ≠ ⊤, then x + y < ⊤.

Русский

Если x ≠ ⊤ и y ≠ ⊤, то x + y < ⊤.

LaTeX

$$$\\\\forall {x,y \\\\in \\\\mathrm{EReal}},\\\\ x \\\\ne \\\\top \\\\land y \\\\ne \\\\top \\\\Rightarrow x + y \\\\lt \\\\top$$$

Lean4

theorem add_lt_top {x y : EReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x + y < ⊤ :=
  add_lt_add hx.lt_top hy.lt_top

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

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

Разделы

Аффилиация

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