atBot_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{atBot}) \\Rightarrow \\operatorname{Tendsto}\\bigl(x \\mapsto f(x) \\cdot r\\bigr) \\, l \\, \\mathrm{atBot}$$$

Lean4

theorem atBot_zsmul_const {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x • r) l atBot :=
  by
  simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢
  exact hf.atTop_zsmul_const hr

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