ofReal_le_natCast

Mathlib.Data.ENNReal.Real

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

English

For nonzero n, n ≤ ENNReal.ofReal p ↔ n ≤ p.

Русский

Для ненулевого n: n ≤ ENNReal.ofReal p ↔ n ≤ p.

LaTeX

$$⟪n ≠ 0⟫ → n ≤ ENNReal.ofReal p ↔ n ≤ p$$

Lean4

@[simp, norm_cast]
theorem ofReal_le_natCast {r : ℝ} {n : ℕ} : ENNReal.ofReal r ≤ n ↔ r ≤ n :=
  coe_le_coe.trans Real.toNNReal_le_natCast

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

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

Разделы

Аффилиация

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