Theorems · Definition · general topology

Filter.IsBounded

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

f.IsBounded r: the filter f is eventually bounded w.r.t. the relation r, i.e. eventually, it is bounded by some uniform bound. r will be usually instantiated with (· ≤ ·) or (· ≥ ·).

Defined in

Mathlib.Order.Filter.Defs

Cited by

45 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms