tendsto_const_mul_atBot_of_neg — Mathlib

English

Let α be an ordered field and l a filter. If r < 0, then Tendsto (x ↦ r · f(x)) along l to −∞ is equivalent to Tendsto f along l to +∞.

Русский

Пусть α — упорядоченное поле и l — фильтр. Пусть r < 0. Тогда Tendsto (x ↦ r · f(x)) вдоль l к −∞ эквивалентно Tendsto f вдоль l к +∞.

LaTeX

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

Lean4

/-- If `r` is a negative constant, `fun x ↦ r * f x` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`. -/
theorem tendsto_const_mul_atBot_of_neg (hr : r < 0) : Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop := by
  simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)

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