exists_add_lt_of_add_lt

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

If y + z < x for ENNReal numbers, there exist y' > y and z' > z with y' + z' < x.

Русский

Если y + z < x для ENNReal, то найдутся y' > y и z' > z такие, что y' + z' < x.

LaTeX

$$$ y + z < x \Rightarrow \exists y' > y, \exists z' > z,\ y' + z' < x $$$

Lean4

theorem exists_add_lt_of_add_lt {x y z : ℝ≥0∞} (h : y + z < x) : ∃ y' > y, ∃ z' > z, y' + z' < x :=
  by
  contrapose! h
  simpa using le_iInf₂_add_iInf₂ h

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

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

Разделы

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

Аффилиация

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