Theorems · Theorem · general topology

Filter.isCoboundedUnder_ge_of_eventually_le

∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α},
  (∀ᶠ (i : ι) in l, f i ≤ x) → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) l f

Defined in

Mathlib.Order.Filter.IsBounded

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderFilter.NeBot