English
For a commutative group G with a partial order and IsOrderedMonoid structure, and a filter l on α, if f, g: α → G satisfy that C ≤ f x eventually for some C, and g(x) tends to atTop, then x ↦ f(x) g(x) tends to atTop.
Русский
Для абелева группы G с частичным порядком и структурой IsOrderedMonoid, и фильтра l на α, если функции f, g: α → G удовлетворяют условию, что существует C сutt, что C ≤ f(x) позднее, и g(x) стремится к atTop, тогда x ↦ f(x) g(x) стремится к atTop.
LaTeX
$$$\\forall l:\\Filter\\ α,\\ \\forall f,g:\\alpha\\to G,\\ \\exists C: G,\\ (\\forall^\\infty x\\in l, C \\le f(x))\\ \\land\\ (\\mathrm{Tendsto}\\ g\\ l\\ atTop)\\Rightarrow \\mathrm{Tendsto}(\\lambda x, f(x) g(x))\\ l\\ atTop$$$
Lean4
@[to_additive]
theorem tendsto_atBot_mul_left_of_ge' (C : G) (hf : ∀ᶠ x in l, f x ≤ C) (hg : Tendsto g l atBot) :
Tendsto (fun x => f x * g x) l atBot :=
tendsto_atTop_mul_left_of_le' (G := Gᵒᵈ) _ C hf hg
