tendsto_mul_const_atTop_iff_pos — Mathlib

English

If f tends to infinity along a nonempty filter l and r > 0, then f(x) · r tends to infinity along l, and conversely.

Русский

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

LaTeX

$$$\operatorname{Tendsto}(f)\ l\ atTop \Rightarrow \operatorname{Tendsto}(x \mapsto f(x) \cdot r)\ l\ atTop \\ \\ \operatorname{Tendsto}(x \mapsto f(x) \cdot r)\ l\ atTop \Rightarrow 0 < r$$$

Lean4

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

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