liminf_add_top_of_ne_bot

Mathlib.Topology.Instances.EReal.Lemmas

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

← MathLib Explorer

English

If liminf u f = ⊤ and liminf v f ≠ ⊥, then liminf (u+v) f = ⊤.

Русский

Если liminf u f = ∞ и liminf v f ≠ ⊥, то liminf(u+v) f = ∞.

LaTeX

$$$ (\liminf u f = \top) \land (\liminf v f \neq \bot) \Rightarrow \liminf (u+v) f = \top $$$

Lean4

theorem liminf_add_top_of_ne_bot (h : liminf u f = ⊤) (h' : liminf v f ≠ ⊥) : liminf (u + v) f = ⊤ :=
  by
  apply top_le_iff.1 (le_trans _ le_liminf_add)
  rw [h, top_add_of_ne_bot h']

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

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

Разделы

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

Аффилиация

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