atTop_nsmul_neg_const — Mathlib

English

Let l be a filter on α, f: α → ℕ, and r ∈ R with r < 0. If f tends to +∞ along l, then f(x) · r tends to the bottom along l.

Русский

Пусть l — фильтр на α, f: α → ℕ и r ∈ R такой, что 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 \\text{ toBot}$$$

Lean4

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

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