bliminf_eq

Mathlib.Order.LiminfLimsup

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

English

Equality for bliminf mirrors the supremum characterization with a bound from below along f under p.

Русский

Равенство bliminf: супремум значений a, для которых p(x) → a ≤ u(x) держится хвостом.

LaTeX

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

Lean4

theorem bliminf_eq : bliminf u f p = sSup {a | ∀ᶠ x in f, p x → a ≤ u x} :=
  rfl

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

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

Разделы

Аффилиация

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