English
For a function into a cancellative ordered monoid, taking natural multiples tends to infinity when the function does and the multiplier is positive.
Русский
Для функции в связанном упорядоченном мониде, умножение на положительное число натуральным образом сохраняет тенденцию к бесконечности.
LaTeX
$$$\forall f:\
\alpha \to \mathbb{N},\; \mathrm{Tendsto} f\ l\ \mathrm{atTop} \Rightarrow \mathrm{Tendsto}(n \mapsto f(n) \cdot r)\ l\ \mathrm{atTop}$$$
Lean4
/-- If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
given in `Filter.Tendsto.atTop_mul_const`). -/
theorem atTop_mul_const' (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atTop :=
by
refine tendsto_atTop.2 fun b => ?_
obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn
filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx
calc
b ≤ max b 0 * 1 := by {
rw [mul_one]
exact le_max_left _ _
}
_ ≤ max b 0 * (n * r) := by gcongr
_ = max b 0 * n * r := by rw [mul_assoc]
_ ≤ f x * r := by gcongr
