English
If the lower linear growth infimum of u is positive, then u tends to the top element of the extended real line.
Русский
Если нижний линейный инф GrowthInf последовательности u положителен, то она стремится к верхней границе объемлющей вещественной плоскости.
LaTeX
$$$\text{If } 0 < \operatorname{linearGrowthInf} u, \ \operatorname{Tendsto} u \ \text{atTop} \ (\mathcal{N}_{\top})$$$
Lean4
theorem tendsto_atTop_of_linearGrowthInf_pos (h : 0 < linearGrowthInf u) : Tendsto u atTop (𝓝 ⊤) :=
by
obtain ⟨a, a_0, a_v⟩ := exists_between h
apply tendsto_nhds_top_mono _ ((le_linearGrowthInf_iff (u := u)).1 (le_refl _) a a_v)
refine tendsto_nhds_top_iff_real.2 fun M ↦ eventually_atTop.2 ?_
lift a to ℝ using ⟨ne_top_of_lt a_v, ne_bot_of_gt a_0⟩
rw [EReal.coe_pos] at a_0
obtain ⟨n, hn⟩ := exists_nat_ge (M / a)
refine ⟨n + 1, fun k k_n ↦ ?_⟩
rw [← coe_coe_eq_natCast, ← coe_mul, EReal.coe_lt_coe_iff, mul_comm]
exact (div_lt_iff₀ a_0).1 (hn.trans_lt (Nat.cast_lt.2 k_n))
