limsup_of_not_isBoundedUnder — Mathlib

English

Let f be a filter on ι and let u : ι → ℝ≥0. If u is not bounded above along f (i.e., not IsBoundedUnder (≤) along f), then the limsup of u along f is 0.

Русский

Пусть f — фильтр на индексы ι, а u : ι → ℝ≥0. Если u не ограничено сверху вдоль f, то limsup u по f равен 0.

LaTeX

$$$\\\\forall f : \\text{Filter } ι, \\\\neg f.IsBoundedUnder (\\\\le) u \\\\Rightarrow \\\\ limsup u f = 0$$$

Lean4

@[simp]
theorem limsup_of_not_isBoundedUnder (hf : ¬f.IsBoundedUnder (· ≤ ·) u) : limsup u f = 0 :=
  limsSup_of_not_isBounded hf

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