atBot_div_const — Mathlib

English

If a function tends to negative infinity along a filter, then dividing by a positive constant preserves this tendency.

Русский

Если функция стремится к минус бесконечности вдоль фильтра, деление на положительную константу сохраняет это стремление.

LaTeX

$$$0 < r \land \operatorname{Tendsto}(f, l, \operatorname{atBot}) \Rightarrow \operatorname{Tendsto}\left(x \mapsto \frac{f(x)}{r}, l, \operatorname{atBot}\right)$$$

Lean4

/-- If a function `f` tends to negative infinity along a filter, then `f` divided by
a positive constant also tends to negative infinity. -/
theorem atBot_div_const (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x / r) l atBot :=
  (tendsto_div_const_atBot_of_pos hr).2 hf

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