of_frequently_ge — Mathlib

English

Let α be a linearly ordered set. If there exists a frequently occurring lower bound a with respect to u, then u is cobounded under ≤ along f; i.e., there exists b ∈ α such that { x ∈ I | b ≤ u(x) } ∈ f.

Русский

Пусть α упорядочено линейно. Если существует предел снизу, встречающийся часто по f, то u является ограниченным ниже по отношению к f; т.е. существует b ∈ α такое, что { x ∈ I | b ≤ u(x) } принадлежит f.

LaTeX

$$$\exists b \in \alpha,\ {x \in \iota \mid b \le u(x)\} \in f$$$

Lean4

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

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