one_le_ofReal

Mathlib.Data.ENNReal.Real

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

English

1 ≤ ENNReal.ofReal p iff 1 ≤ p.

Русский

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

LaTeX

$$1 ≤ ENNReal.ofReal p \iff 1 ≤ p$$

Lean4

@[simp]
theorem one_le_ofReal {p : ℝ} : 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p := by exact mod_cast natCast_le_ofReal one_ne_zero

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

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

Разделы

Аффилиация

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