tendsto_div_const_atBot_of_neg — Mathlib

English

Let α be an ordered field and l a nontrivial 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}\left(x \mapsto \frac{f(x)}{r}\right)\ l\ aBot \Leftrightarrow \operatorname{Tendsto} f\ l\ aTop $$$$

Lean4

/-- If `r` is a negative constant, `fun x ↦ f x / r` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`. -/
theorem tendsto_div_const_atBot_of_neg (hr : r < 0) : Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atTop := by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_neg, hr]

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