limsSup — Mathlib

English

For a function u and a filter f, the limsup of u along f is the greatest lower bound (infimum) of all bounds a such that u(n) ≤ a eventually holds along f.

Русский

Для функции u и фильтра f предел верхний limsup — наибольший нижний предел всех ограничений a, при которых u(n) ≤ a выполняется для большого n.

LaTeX

$$$\limsup_{f} u = \inf\{a : \forall^\!\! n \in f,\ u(n) \le a\}$$$

Lean4

/-- The `limsSup` of a filter `f` is the infimum of the `a` such that the inequality
`x ≤ a` eventually holds for `f`. -/
def limsSup (f : Filter α) : α :=
  sInf {a | ∀ᶠ n in f, n ≤ a}

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