toNNReal_le_toNNReal_iff_of_pos

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Real.toNNReal_le_toNNReal_iff_of_pos

English

If r > 0, then r.toNNReal ≤ p.toNNReal iff r ≤ p.

Русский

Пусть r > 0, тогда r.toNNReal ≤ p.toNNReal эквивалентно r ≤ p.

LaTeX

$$$$ 0 < r \implies \operatorname{toNNReal}(r) \le \operatorname{toNNReal}(p) \iff r \le p. $$$$

Lean4

theorem toNNReal_le_toNNReal_iff_of_pos {r p : ℝ} (hr : 0 < r) : r.toNNReal ≤ p.toNNReal ↔ r ≤ p := by
  simp [toNNReal_le_toNNReal_iff', hr.not_ge]

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

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

Разделы

Аффилиация

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