toReal_eq_zero_iff

Mathlib.Data.EReal.Basic

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

English

The real part of x is zero exactly when x equals 0, ⊤, or ⊥.

Русский

Реальная часть x равна нулю тогда и только тогда, когда x = 0, ⊤ или ⊥.

LaTeX

$$$x.toReal = 0 \iff x = 0 \lor x = \top \lor x = \bot$$$

Lean4

theorem toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥ := by cases x <;> norm_num

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

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

Разделы

Аффилиация

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