atTop_mul_atTop₀ — Mathlib

English

If f and g tend to atTop along l, then the product f(x)·g(x) tends to atTop.

Русский

Если f и g сходятся к atTop по фильтру l, то произведение f(x)·g(x) сходится к atTop.

LaTeX

$$$$ \operatorname{Tendsto}\; f\; l\; \operatorname{atTop} \Rightarrow\; \operatorname{Tendsto}\; g\; l\; \operatorname{atTop} \Rightarrow \operatorname{Tendsto}(x \mapsto f(x)g(x))\; l\; \operatorname{atTop} $$$$

Lean4

theorem atTop_mul_atTop₀ (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop :=
  by
  refine tendsto_atTop_mono' _ ?_ hg
  filter_upwards [hg.eventually (eventually_ge_atTop 0), hf.eventually (eventually_ge_atTop 1)] with _ using
    le_mul_of_one_le_left

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