liminf_add_gt_of_gt

Mathlib.Topology.Instances.EReal.Lemmas

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

← MathLib Explorer

English

If a < liminf u f and b < liminf v f, then a+b < liminf (u+v) f.

Русский

Если a < liminf u f и b < liminf v f, то a+b < liminf (u+v) f.

LaTeX

$$$ (a < \liminf u f) \land (b < \liminf v f) \Rightarrow a+b < \liminf (u+v) f $$$

Lean4

theorem liminf_add_gt_of_gt {a b : EReal} (ha : a < liminf u f) (hb : b < liminf v f) : a + b < liminf (u + v) f :=
  (add_lt_add ha hb).trans_le le_liminf_add

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

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

Разделы

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

Аффилиация

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