Theorems · Definition · general topology

Filter.IsBoundedUnder

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

f.IsBoundedUnder (≺) u: the image of the filter f under u is eventually bounded w.r.t. the relation ≺, i.e. eventually, it is bounded by some uniform bound.

Defined in

Mathlib.Order.Filter.Defs

Cited by

247 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 27 definitions · uses no axioms