coe_toNNReal_le

Mathlib.Data.NNReal.Defs

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

English

For all x ∈ ℝ, (toNNReal x) ≤ |x| (as real).

Русский

Для всех x ∈ ℝ, (toNNReal x) ≤ |x| (в действительных).

LaTeX

$$$ (toNNReal x : \mathbb{R}) \le |x|. $$$

Lean4

theorem coe_toNNReal_le (x : ℝ) : (toNNReal x : ℝ) ≤ |x| :=
  max_le (le_abs_self _) (abs_nonneg _)

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

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

Разделы

Аффилиация

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