tendsto_nhds_top_iff_natCast_lt — Mathlib

English

Tendsto f to top in ENat is equivalent to: for all n ∈ ℕ, eventually n < f(a).

Русский

Сходится к верхнему пределу в ENat тогда и только тогда, когда для каждого n ∈ ℕ тождественно выполняется n < f(a) eventually.

LaTeX

$$$$\\forall \\alpha, \\; \\operatorname{Tendsto}(f,l,\\mathcal{N}_{\\top}) \\iff \\forall n \\in \\mathbb{N}, \\; \\text{eventually } (n < f(a)).$$$$

Lean4

theorem tendsto_nhds_top_iff_natCast_lt {α : Type*} {l : Filter α} {f : α → ℕ∞} :
    Tendsto f l (𝓝 ⊤) ↔ ∀ n : ℕ, ∀ᶠ a in l, n < f a := by
  simp_rw [nhds_top_order, lt_top_iff_ne_top, tendsto_iInf, tendsto_principal, ENat.forall_ne_top, mem_Ioi]

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