le_toNNReal_of_coe_le

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.le_toNNReal_of_coe_le

English

If x ∈ ℝ≥0 and y ∈ ℝ with x ≤ y, then x ≤ y.toNNReal.

Русский

Если x ∈ ℝ≥0 и y ∈ ℝ, и x ≤ y, то x ≤ y.toNNReal.

LaTeX

$$$\forall x \in \mathbb{R}_{\ge 0},\forall y \in \mathbb{R},\ x \le y\Rightarrow x \le y^{\mathbb{NNReal}}$$$

Lean4

theorem le_toNNReal_of_coe_le {x : ℝ≥0} {y : ℝ} (h : ↑x ≤ y) : x ≤ y.toNNReal :=
  (le_toNNReal_iff_coe_le <| x.2.trans h).2 h

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

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

Разделы

Аффилиация

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