add_top_iff_ne_bot

Mathlib.Data.EReal.Operations

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

← MathLib Explorer

English

x + ⊤ = ⊤ iff x ≠ ⊥.

Русский

x + ⊤ = ⊤ тогда же и только тогда, когда x ≠ ⊥.

LaTeX

$$$x + \\\\top = \\\\top \\\\Leftrightarrow x \\\\neq \\\\bot$$$

Lean4

/-- For any extended real number `x`, the sum of `x` and `⊤` is equal to `⊤`
if and only if `x` is not `⊥`. -/
theorem add_top_iff_ne_bot {x : EReal} : x + ⊤ = ⊤ ↔ x ≠ ⊥ := by rw [add_comm, top_add_iff_ne_bot]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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