atTop_zsmul_neg_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

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

Lean4

theorem atTop_zsmul_neg_const {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atBot :=
  by simpa using hf.atTop_zsmul_const (neg_pos.2 hr)

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