tendsto_mul_const_atTop_of_neg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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