tendsto_zero — Mathlib

English

A map f from a set to Γ₀ tends to 0 iff eventually f(x) is less than every nonzero γ in Γ₀.

Русский

Функция f из множества X в Γ₀ стремится к 0 тогда и только тогда, когда неотсроченно выполняются неравенства f(x) < γ для каждого γ ≠ 0.

LaTeX

$$$\operatorname{Tendsto} f\, l\,(\mathcal{N}(0)) \;\Leftrightarrow\; \forall γ₀, γ₀ \neq 0, \forall^\! x \in l, f(x) < γ₀$$$

Lean4

theorem tendsto_zero : Tendsto f l (𝓝 (0 : Γ₀)) ↔ ∀ (γ₀) (_ : γ₀ ≠ 0), ∀ᶠ x in l, f x < γ₀ := by simp [nhds_zero]

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