atTop_mul_const_of_neg' — Mathlib

English

If a positive, archimedean-invoking constant r is negative, there is a related negation-tracked version of the Tendsto result for null directions.

Русский

Если константа r отрицательна, существует формулировка результатов предельности с учетом отрицания.

LaTeX

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

Lean4

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

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