tendsto_nhds_top — Mathlib

English

If a function m dominates every natural bound along a filter f, then m tends to ∞. Concretely, if for all natural numbers n we have ↑n < m a eventually, then Tendsto m f (𝓝 ∞).

Русский

Если функция m превзходит все натуральные границы вдоль фильтра f, то m стремится к бесконечности. Конкретно, если для каждого натурального числа n верно, что ↑n < m a в пределе f, тогда Tendsto m f (nhds ∞).

LaTeX

$$$\\text{(гипотеза)} \\forall n \\in \\mathbb{N}, \\forall^{\\infty} a \\in f, \\uparrow n < m a \\Rightarrow \\operatorname{Tendsto} m f (\\mathcal{N}(\\infty))$$$

Lean4

theorem tendsto_nhds_top {m : α → ℝ≥0∞} {f : Filter α} (h : ∀ n : ℕ, ∀ᶠ a in f, ↑n < m a) : Tendsto m f (𝓝 ∞) :=
  tendsto_nhds_top_iff_nat.2 h

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