ofReal_add_le

Mathlib.Data.ENNReal.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.ofReal_add_le

English

For real p,q, ENNReal.ofReal(p+q) ≤ ENNReal.ofReal(p) + ENNReal.ofReal(q).

Русский

Для любых p,q ∈ ℝ: ENNReal.ofReal(p+q) ≤ ENNReal.ofReal(p) + ENNReal.ofReal(q).

LaTeX

$$$\\text{ofReal}(p+q) \\le \\text{ofReal}(p) + \\text{ofReal}(q)$$$

Lean4

theorem ofReal_add_le {p q : ℝ} : ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q :=
  coe_le_coe.2 Real.toNNReal_add_le

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

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

Разделы

Аффилиация

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