Theorems · Theorem · general topology

Filter.IsCobounded.of_frequently_le

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

In linear orders, frequent boundedness from above implies coboundedness for ≥.

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

3 results in Mathlib

Foundations

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

Assumes

LinearOrder