frequently_le — Mathlib

English

For nontrivial linear orders, coboundedness for ≥ implies frequent upper-bounding from above.

Русский

Для ненулевого линейного порядка кобундированность по ≥ влечёт частотное ограничение сверху.

LaTeX

$$$\text{If } f \text{ is cobounded under } (\ge) \text{ on a linear order, then } \exists u, \exists^\! x \in f, x \le u.$$$

Lean4

/-- For nontrivial filters in linear orders, coboundedness for `≥` implies frequent boundedness
from above. -/
theorem frequently_le [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≥ ·) f) : ∃ u, ∃ᶠ x in f, x ≤ u :=
  cobdd.frequently_ge (α := αᵒᵈ)

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