tendsto_const_mul_atBot_iff_pos — Mathlib

English

If f tends to +∞ along a nontrivial l, then Tendsto (x ↦ f(x) · r) l atBot is equivalent to r < 0.

Русский

Если f стремится к +∞ по не тривиальному l, то Tendsto (x ↦ f(x) · r) l к −∞ эквивалентно r < 0.

LaTeX

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

Lean4

/-- If `f` tends to negative infinity along a nontrivial filter `l`, then
`fun x ↦ r * f x` tends to negative infinity if and only if `0 < r`. -/
theorem tendsto_const_mul_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) :
    Tendsto (fun x => r * f x) l atBot ↔ 0 < r := by
  simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]

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