atBot_mul_neg — Mathlib

English

In a linearly ordered field, the reciprocal map sends the neighborhood basis at 0 from the left to the atBot filter, i.e., inv atBot = nhds<0.

Русский

Обратное отображение отправляет окрестности нуля слева в atBot.

LaTeX

$$$(\mathrm{atBot})^{-1} = \mathcal{N}_{<0}(0).$$$

Lean4

/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atBot` and `g`
tends to a negative constant `C` then `f * g` tends to `Filter.atTop`. -/
theorem atBot_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x * g x) l atTop :=
  by
  have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg
  simpa [Function.comp_def] using tendsto_neg_atBot_atTop.comp this

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