English
Let α be a linearly ordered set and f a nontrivial filter on an index set. If a function u: I → α is cobounded above along f, then there exists a bound a ∈ α such that the set { x ∈ I | u(x) ≤ a } belongs to f (i.e., u is frequently bounded above by a).
Русский
Пусть α упорядочено линейно, f — непустой фильтр на некотором индексе I, и u: I → α. Если u ограничено сверху вдоль f, то существует элемент a ∈ α such that множество { x ∈ I | u(x) ≤ a } принадлежит f (уже часто выполняется условие).
LaTeX
$$$\exists a \in \alpha,\ {x \in \iota \mid u(x) \le a\} \in f$$$
Lean4
theorem frequently_le [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α} (h : IsCoboundedUnder (· ≥ ·) f u) :
∃ a, ∃ᶠ x in f, u x ≤ a :=
IsCobounded.frequently_le h
