Theorems · Definition · general topology

Filter.IsCobounded

{α : Type u_1} → (α → α → Prop) → Filter α → Prop

IsCobounded (≺) f states that the filter f does not tend to infinity w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated with ≤ or ≥. There is a subtlety in this definition: we want f.IsCobounded to hold for any f in the case of complete lattices. This will be relevant to deduce theorems on complete lattices from their versions on conditionally complete lattices with additional assumptions. We have to be careful in the edge case of the trivial filter containing the empty set: the other natural definition ¬ ∀ a, ∀ᶠ n in f, a ≤ n would not work as well in this case.

Defined in

Mathlib.Order.Filter.Defs

Cited by

42 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms