tendsto_nhds_zero — Mathlib

English

A net tends to 0 in ENNReal iff for every ε>0, eventually the net is ≤ ε.

Русский

Сеть стремится к 0 в ENNReal тогда и только тогда, когда для каждого ε>0 в итоге сеть меньше равна ε.

LaTeX

$$$\\text{Tendsto }u f (\\mathcal{N}0) \\iff \\forall ε>0, \\forall^f x, u(x) ≤ ε$$$

Lean4

protected theorem tendsto_nhds_zero {f : Filter α} {u : α → ℝ≥0∞} : Tendsto u f (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in f, u x ≤ ε :=
  nhds_zero_basis_Iic.tendsto_right_iff

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