tendsto_const_mul_atBot_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}(x \mapsto f(x) / 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 infinity along a nontrivial filter,
`fun x ↦ r * f x` tends to negative infinity if and only if `r < 0`. -/
theorem tendsto_const_mul_atBot_iff_neg [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x => r * f x) l atBot ↔ r < 0 := by
  simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atTop_atBot]

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