toENNReal_add_le

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.toENNReal_add_le

← MathLib Explorer

English

(x + y).toENNReal ≤ x.toENNReal + y.toENNReal for all x,y.

Русский

(x+y).toENNReal \\\\le x.toENNReal + y.toENNReal для любых x,y.

LaTeX

$$$ (x+y).toENNReal \\\\le x.toENNReal + y.toENNReal $$$

Lean4

theorem toENNReal_add_le {x y : EReal} : (x + y).toENNReal ≤ x.toENNReal + y.toENNReal :=
  by
  induction x <;> induction y <;>
    try { · simp
    }
  exact ENNReal.ofReal_add_le

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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