atBot_mul_const_of_neg' — Mathlib

English

Analogous to the top variant for bottom; multiplying by a negative constant on the right swaps atTop to atBot in Tendsto sense.

Русский

Аналогично верхней версии для нижней части; умножение на отрицательную константу справа переводит atTop в atBot.

LaTeX

$$$\forall r<0\;\mathrm{Tendsto}\ f\ l\ \mathrm{atBot} \Rightarrow \mathrm{Tendsto}(x \mapsto f(x) \cdot r)\ l\ atTop$$$

Lean4

/-- See also `Filter.Tendsto.atBot_mul_const_of_neg` for a version of this lemma for
`LinearOrderedField`s which does not require the `Archimedean` assumption. -/
theorem atBot_mul_const_of_neg' (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop := by
  simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)

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