add_ne_bot_iff

Mathlib.Data.EReal.Operations

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

English

x + y ≠ ⊥ if and only if x ≠ ⊥ and y ≠ ⊥.

Русский

x + y ≠ ⊥ тогда и только тогда, когда x ≠ ⊥ и y ≠ ⊥.

LaTeX

$$$\\\\forall {x,y \\\\in \\\\mathrm{EReal}},\\\\ x+y \\\\neq \\\\bot \iff x \\\\neq \\\\bot \land y \\\\neq \\\\bot$$$

Lean4

theorem add_ne_bot_iff {x y : EReal} : x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥ :=
  WithBot.add_ne_bot

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

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

Разделы

Аффилиация

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