atTop_nsmul_const — Mathlib

English

If r > 0 and f tends to atTop along a filter l, then x ↦ f(x) • r tends to atTop as well.

Русский

Если r > 0 и f стремится к бесконечности вдоль фильтра l, тогда x ↦ f(x) • r также стремится к бесконечности.

LaTeX

$$∀ {f : α → ℕ} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atTop$$

Lean4

theorem atTop_nsmul_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
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

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