toNNReal_lt_toNNReal_iff_of_nonneg

Mathlib.Data.NNReal.Defs

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

← MathLib Explorer

English

If r ≥ 0, then toNNReal r < toNNReal p iff r < p.

Русский

Пусть r ≥ 0. Тогда toNNReal r < toNNReal p эквивалентно r < p.

LaTeX

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

Lean4

theorem toNNReal_lt_toNNReal_iff_of_nonneg {r p : ℝ} (hr : 0 ≤ r) : Real.toNNReal r < Real.toNNReal p ↔ r < p :=
  toNNReal_lt_toNNReal_iff'.trans ⟨And.left, fun h => ⟨h, lt_of_le_of_lt hr h⟩⟩

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

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

Разделы

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

Аффилиация

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