ofReal_le_ofNat

Mathlib.Data.ENNReal.Real

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

English

For real r and n ∈ ℕ with n ≥ 2, ENNReal.ofReal r ≤ ofReal(n) iff r ≤ n.

Русский

Для действительного r и n ∈ ℕ с n ≥ 2: ENNReal.ofReal r ≤ ofReal n ↔ r ≤ n.

LaTeX

$$∀ {r : Real} {n : Nat} [n.AtLeastTwo], ENNReal.ofReal r ≤ ENNReal.ofReal n.cast ↔ r ≤ n.cast$$

Lean4

@[simp]
theorem ofReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] : ENNReal.ofReal r ≤ ofNat(n) ↔ r ≤ OfNat.ofNat n :=
  ofReal_le_natCast

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

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

Разделы

Аффилиация

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