toNNReal_le_toNNReal

Mathlib.Data.NNReal.Defs

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

English

For all r ≤ p, we have toNNReal(r) ≤ toNNReal(p).

Русский

Для всех r ≤ p выполняется toNNReal(r) ≤ toNNReal(p).

LaTeX

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

Lean4

theorem toNNReal_le_toNNReal {r p : ℝ} (h : r ≤ p) : Real.toNNReal r ≤ Real.toNNReal p :=
  Real.toNNReal_mono h

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

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

Разделы

Аффилиация

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