Theorems · Definition · general topology

Filter.ZeroAtFilter

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

If l is a filter on α, then a function f : α → β is ZeroAtFilter l if it tends to zero along l.

Defined in

Mathlib.Order.Filter.ZeroAndBoundedAtFilter

Cited by

11 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

ZeroTopologicalSpace