tendsto_div_const_atTop_iff_pos — Mathlib

English

If f tends to infinity along a filter l, then for any r, Tendsto f l atTop implies Tendsto (x ↦ f(x)/r) l atTop if and only if r > 0.

Русский

Если f идёт к бесконечности вдоль фильтра l, тогда для любого r, Tendsto f l atTop эквивалентно Tendsto (f(x)/r) l atTop при условии r > 0.

LaTeX

$$$\text{Tendsto}(f)\ l\ atTop \Rightarrow \big( \text{Tendsto}(x \mapsto f(x)/r)\ l\ atTop \iff 0 < r \big)$$$

Lean4

/-- If `f` tends to infinity along a nontrivial filter `l`, then
`x ↦ f x * r` tends to infinity if and only if `0 < r`. -/
theorem tendsto_div_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) : Tendsto (fun x ↦ f x / r) l atTop ↔ 0 < r :=
  by simp only [div_eq_mul_inv, tendsto_mul_const_atTop_iff_pos h, inv_pos]

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