tendsto_atTop_mul_left_of_le — Mathlib

English

In the setting of a commutative group G with order, the following holds: if l is a filter on α and for all x there exists C with C ≤ f x, then Tendsto (f x · g x) toTop whenever Tendsto g toTop holds.

Русский

В условиях группы G с порядком: если l — фильтр на α и для каждой x есть C, удовлетворяющее C ≤ f(x), тогда при Tendsto g к atTop имеет место Tendsto (f(x) g(x)) к atTop.

LaTeX

$$$\\forall l:\\Filter\\ α,\\ \\forall f,g:\\alpha\\to G,\\ (\\forall x, C \\le f(x))\\Rightarrow \\mathrm{Tendsto}(f\\cdot g)\\ l\\ atTop$$$

Lean4

@[to_additive]
theorem tendsto_atTop_mul_left_of_le (C : G) (hf : ∀ x, C ≤ f x) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mul_left_of_le' l C (univ_mem' hf) hg

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