tendsto_div_const_atTop_iff_neg — Mathlib

English

For nontrivial l, Tendsto (x ↦ f(x) / r) l atTop is equivalent to r > 0 and Tendsto f l atTop or r < 0 and Tendsto f l atBot.

Русский

Для непустого l: Tendsto (x ↦ f(x) / r) l к +∞ эквивалентно r > 0 и Tendsto f к +∞ или r < 0 и Tendsto f к −∞.

LaTeX

$$$$ \operatorname{Tendsto}\left(x \mapsto \frac{f(x)}{r}\right) l aTop \Leftrightarrow (0 < r \land \operatorname{Tendsto} f l aTop) \lor (r < 0 \land \operatorname{Tendsto} f l aBot) $$$$

Lean4

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

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