ofReal_pos

Mathlib.Data.ENNReal.Real

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

English

For every real p, ENNReal.ofReal p is positive if and only if p is positive.

Русский

Для каждого p ∈ ℝ выполнено: ENNReal.ofReal p > 0 тогда и только если p > 0.

LaTeX

$$$ 0 < ENNReal.ofReal p \iff 0 < p $$$

Lean4

@[simp]
theorem ofReal_pos {p : ℝ} : 0 < ENNReal.ofReal p ↔ 0 < p := by simp [ENNReal.ofReal]

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

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

Разделы

Аффилиация

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