Theorems · Definition · general topology

Filter.BoundedAtFilter

{α : Type u_2} → {β : Type u_3} → [Norm β] → Filter α → (α → β) → Prop

If l is a filter on α, then a function f: α → β is BoundedAtFilter l if f =O[l] 1.

Defined in

Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Cited by

14 results in Mathlib

Foundations

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

Assumes

Norm