ZeroAtFilter — Mathlib

English

If l is a filter on α, then the function f tends to zero along l exactly when f converges to 0 in the topological sense along l.

Русский

Если l — фильтр на α, то функция f стремится к нулю вдоль l тогда и только тогда, когда она в топологическом смысле сходится к 0 вдоль l.

LaTeX

$$$\\mathrm{ZeroAtFilter}(l,f) \\iff \\mathrm{Tendsto}(f,l, \\mathcal{N}(0))$$$

Lean4

/-- If `l` is a filter on `α`, then a function `f : α → β` is `ZeroAtFilter l`
  if it tends to zero along `l`. -/
def ZeroAtFilter [Zero β] [TopologicalSpace β] (l : Filter α) (f : α → β) : Prop :=
  Filter.Tendsto f l (𝓝 0)

Похожие утверждения