Theorems · Theorem · general topology

Filter.IsCobounded.frequently_le

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

For nontrivial filters in linear orders, coboundedness for ≥ implies frequent boundedness from above.

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