toNNReal_le_toNNReal_iff

Mathlib.Data.NNReal.Defs

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

English

For real r and p with p ≥ 0, toNNReal r ≤ toNNReal p iff r ≤ p.

Русский

Для действительных r и p ≥ 0: toNNReal r ≤ toNNReal p ⇔ r ≤ p.

LaTeX

$$$$ p \\ge 0 \\Rightarrow toNNReal\\,r \\le toNNReal\\,p \\iff r \\le p. $$$$

Lean4

@[simp]
theorem toNNReal_le_toNNReal_iff {r p : ℝ} (hp : 0 ≤ p) : toNNReal r ≤ toNNReal p ↔ r ≤ p := by
  simp [← NNReal.coe_le_coe, hp]

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

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

Разделы

Аффилиация

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