iInf_le_liminf

Mathlib.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#Filter.iInf_le_liminf

← MathLib Explorer

English

The infimum over n of u(n) is less than or equal to liminf u f: ⨅ n, u n ≤ liminf u f.

Русский

Наименьшее по n меньше или равно лиминфу: ⨅ n, u n ≤ liminf u f.

LaTeX

$$$\\bigwedge_{n} u(n) \\le \\liminf u f$$$

Lean4

theorem iInf_le_liminf {f : Filter β} {u : β → α} : ⨅ n, u n ≤ liminf u f :=
  le_liminf_of_le (by isBoundedDefault) (Eventually.of_forall (iInf_le u))

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

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

Разделы

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

Аффилиация

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