zero_eq_ofReal

Mathlib.Data.ENNReal.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.zero_eq_ofReal

English

0 = ENNReal.ofReal p iff p ≤ 0.

Русский

0 = ENNReal.ofReal p тогда и только если p ≤ 0.

LaTeX

$$$ 0 = ENNReal.ofReal p \iff p \le 0 $$$

Lean4

@[simp]
theorem zero_eq_ofReal {p : ℝ} : 0 = ENNReal.ofReal p ↔ p ≤ 0 :=
  eq_comm.trans ofReal_eq_zero

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

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

Разделы

Аффилиация

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