English
If f: N → R tends to +∞, then Hyperreal.ofSeq f is InfinitePos.
Русский
Пусть f(n) стремится к +∞; тогда Hyperreal.ofSeq f бесконечно велик по положительной стороне.
LaTeX
$$$\\forall f:\\mathbb{N}\\to \\mathbb{R}, \\mathrm{Tendsto}(f,\\mathrm{atTop},\\mathrm{atTop}) \\rightarrow \\mathrm{InfinitePos}(\\mathrm{ofSeq}(f))$$$
Lean4
theorem infinitePos_of_tendsto_top {f : ℕ → ℝ} (hf : Tendsto f atTop atTop) : InfinitePos (ofSeq f) := fun r =>
have hf' := tendsto_atTop_atTop.mp hf
let ⟨i, hi⟩ := hf' (r + 1)
have hi' : ∀ a : ℕ, f a < r + 1 → a < i := fun a => lt_imp_lt_of_le_imp_le (hi a)
have hS : {a : ℕ | r < f a}ᶜ ⊆ {a : ℕ | a ≤ i} :=
by
simp only [Set.compl_setOf, not_lt]
exact fun a har => le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _)))
Germ.coe_lt.2 <| mem_hyperfilter_of_finite_compl <| (Set.finite_le_nat _).subset hS
