toNNReal_le_iff_le_coe

Mathlib.Data.NNReal.Defs

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

English

For all r, p ∈ Real, r.toNNReal ≤ p.toNNReal ↔ (r ≤ p) ∨ (r ≤ 0).

Русский

Для всех r, p ∈ ℝ: r.toNNReal ≤ p.toNNReal эквивалентно (r ≤ p) или (r ≤ 0).

LaTeX

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

Lean4

theorem toNNReal_le_iff_le_coe {r : ℝ} {p : ℝ≥0} : toNNReal r ≤ p ↔ r ≤ ↑p :=
  NNReal.gi.gc r p

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

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

Разделы

Аффилиация

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