le_toNNReal_iff_coe_le'

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Real.le_toNNReal_iff_coe_le'

← MathLib Explorer

English

If r > 0, then r ≤ toNNReal p ↔ ↑r ≤ p.

Русский

Если r > 0, то r ≤ toNNReal p ↔ ↑r ≤ p.

LaTeX

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

Lean4

theorem le_toNNReal_iff_coe_le' {r : ℝ≥0} {p : ℝ} (hr : 0 < r) : r ≤ Real.toNNReal p ↔ ↑r ≤ p :=
  (le_or_gt 0 p).elim le_toNNReal_iff_coe_le fun hp => by
    simp only [(hp.trans_le r.coe_nonneg).not_ge, toNNReal_eq_zero.2 hp.le, hr.not_ge]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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