Theorems · Theorem · general topology

Filter.IsCobounded.frequently_ge

∀ {α : Type u_1} {f : Filter α} [inst : LinearOrder α] [f.NeBot],
  Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f → ∃ l, ∃ᶠ (x : α) in f, l ≤ x

For nontrivial filters in linear orders, coboundedness for ≤ implies frequent boundedness from below.

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

3 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderFilter.NeBot