atTop_zsmul_const — Mathlib

English

Let f: α → ℤ and r > 0. If f tends to +∞ along l, then f(x) · r tends to +∞ along l.

Русский

Пусть f: α → ℤ и r > 0. Если f стремится к +∞ вдоль l, то f(x) · r стремится к +∞ вдоль l.

LaTeX

$$$ 0 < r \\land \\operatorname{Tendsto}(f, l, \\mathrm{atTop}) \\Rightarrow \\operatorname{Tendsto}\\bigl(x \\mapsto f(x) \\cdot r\\bigr) \\, l \\, \\mathrm{atTop}$$$

Lean4

theorem atTop_zsmul_const {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atTop :=
  by
  refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  replace hn : s ≤ (n : ℤ) • r := by simpa
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

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