bot_lt_add_iff

Mathlib.Data.EReal.Operations

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

English

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

Русский

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

LaTeX

$$$\\\\bot < x+y \\\\iff \\\\bot < x \\\\land \\\\bot < y$$$

Lean4

@[simp]
theorem bot_lt_add_iff {x y : EReal} : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y := by simp [bot_lt_iff_ne_bot]

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

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

Разделы

Аффилиация

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