liminf_eq

Mathlib.Order.LiminfLimsup

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

English

Equality for limsup along f with the corresponding sup/inf characterizations holds exactly as declared in the definitions.

Русский

Равенство limsup в терминах опорных множеств выполняется точно как в определениях.

LaTeX

$$$\limsup u f = \inf\{a : \forall^\infty x\in f, u(x) ≤ a\}$$$

Lean4

theorem liminf_eq : liminf u f = sSup {a | ∀ᶠ n in f, a ≤ u n} :=
  rfl

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

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

Разделы

Аффилиация

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