limsup_eq

Mathlib.Order.LiminfLimsup

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

English

Equality for bliminf mirrors the defining supremum of a family of bounds under the predicate p along the filter.

Русский

Равенство bliminf повторяет определение супремума по множеству ограничений.

LaTeX

$$$\operatorname{bliminf} u f p = \sup\{a : \forall^\infty x\in f,\ p(x) \to a ≤ u(x)\}$$$

Lean4

theorem limsup_eq : limsup u f = sInf {a | ∀ᶠ n in f, u n ≤ a} :=
  rfl

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

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

Разделы

Аффилиация

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