frequently_ge — Mathlib

English

In linear orders, frequently bound below under IsCoboundedUnder implies the cobounded property for ≥.

Русский

В линейных порядках, частотное ограничение снизу под IsCoboundedUnder влечёт coboundedness по ≥.

LaTeX

$$$\text{In linear orders } IsCoboundedUnder(≤) \; f \; u \Rightarrow \exists a, \exists^\! x \in f, a \le u(x).$$$

Lean4

theorem frequently_ge [LinearOrder α] {f : Filter ι} [NeBot f] {u : ι → α} (h : IsCoboundedUnder (· ≤ ·) f u) :
    ∃ a, ∃ᶠ x in f, a ≤ u x :=
  IsCobounded.frequently_ge h

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