toReal_ne_zero_iff

Mathlib.Data.EReal.Basic

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

English

The real part is nonzero exactly when x is not 0, ⊤, or ⊥.

Русский

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

LaTeX

$$$x.toReal \neq 0 \iff x \neq 0 \\land x \neq \top \\land x \neq \bot$$$

Lean4

theorem toReal_ne_zero_iff {x : EReal} : x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥ := by
  simp only [ne_eq, toReal_eq_zero_iff, not_or]

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

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

Разделы

Аффилиация

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