tendsto_div_const_atBot_iff_pos — Mathlib

English

For nontrivial l, Tendsto (x ↦ f(x) · r) l atTop is equivalent to (0 < r ∧ Tendsto f l atTop) ∨ (r < 0 ∧ Tendsto f l atBot).

Русский

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

LaTeX

$$$$ \operatorname{Tendsto}(x \mapsto f(x) \cdot r) 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 negative infinity if and only if `0 < r`. -/
theorem tendsto_div_const_atBot_iff_pos [NeBot l] (h : Tendsto f l atBot) : Tendsto (fun x ↦ f x / r) l atBot ↔ 0 < r :=
  by simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_pos h]

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