tendsto_div_const_atBot_of_pos — Mathlib

English

If r > 0, Tendsto (x ↦ f(x) / r) l atBot is equivalent to Tendsto f l atBot.

Русский

Если r > 0, Tendsto (x ↦ f(x) / r) l atBot эквивалентно Tendsto f l atBot.

LaTeX

$$$\text{Tendsto}(x \mapsto f(x)/r)\ l\ atBot \iff \text{Tendsto}(f)\ l\ atBot$$$

Lean4

/-- If `r` is a positive constant, `fun x ↦ f x / r` tends to negative infinity along a filter
if and only if `f` tends to negative infinity along the same filter. -/
theorem tendsto_div_const_atBot_of_pos (hr : 0 < r) : Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atBot := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_pos, hr]

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