add_eq_bot_iff

Mathlib.Data.EReal.Operations

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

English

For x,y in EReal, x + y = ⊥ if and only if x = ⊥ or y = ⊥.

Русский

Для x,y в EReal верно: x + y = ⊥ тогда и только тогда, когда x = ⊥ или y = ⊥.

LaTeX

$$$\\\\forall {x,y \\\\in \\\\mathrm{EReal}},\\\\ x+y = \\\\bot \iff x = \\\\bot \lor y = \\\\bot$$$

Lean4

@[simp]
theorem add_eq_bot_iff {x y : EReal} : x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥ :=
  WithBot.add_eq_bot

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

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

Разделы

Аффилиация

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