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