English
Let m be a function from α to ENNReal and f a filter on α. Then m tends to ∞ along f exactly when, for every nonnegative real x, the set of indices a with m(a) exceeding x is eventually true along f.
Русский
Пусть m : α → ENNReal и f — фильтр на α. Тогда m сходится к бесконечности вдоль f тогда и только тогда, когда для каждого неотрицательного элемента x ∈ ℝ≥0 максимум, множество индексов a такое, что m a > x, содержится в f как предельное (т.е. выполняется для всех sufficiently large a).
LaTeX
$$$\\operatorname{Tendsto} m f (\\mathcal{N}(\\infty)) \\iff \\forall x \\in \\mathbb{R}_{\\ge 0}, \\forall^{\\infty} a \\in f, \\uparrow x < m a$$$
Lean4
theorem tendsto_nhds_top_iff_nnreal {m : α → ℝ≥0∞} {f : Filter α} :
Tendsto m f (𝓝 ∞) ↔ ∀ x : ℝ≥0, ∀ᶠ a in f, ↑x < m a := by
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]
