blimsup_eq — Mathlib

English

Equality for blimsup: the blimsup of u along f bounded by p equals the infimum of bounds a with eventual u ≤ a whenever p holds.

Русский

Свойство равенства blimsup: предел верхний с ограничением по p равен инфимума границ a, для которых u ≤ a выполняется хвостами при p.

LaTeX

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

Lean4

theorem blimsup_eq : blimsup u f p = sInf {a | ∀ᶠ x in f, p x → u x ≤ a} :=
  rfl

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