tendsto_atBot_mul_right_of_ge' — Mathlib

English

Let l be a filter on α and G a commutative group with order. If f x ≥ C eventually and g tends to atTop, then x ↦ f(x) g(x) tends to atTop.

Русский

Пусть l — фильтр на α и G — коммутативная группа с порядком. Если f(x) ≥ C позднее и g стремится к atTop, тогда x ↦ f(x) g(x) стремится к atTop.

LaTeX

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

Lean4

@[to_additive]
theorem tendsto_atBot_mul_right_of_ge' (C : G) (hf : Tendsto f l atBot) (hg : ∀ᶠ x in l, g x ≤ C) :
    Tendsto (fun x => f x * g x) l atBot :=
  tendsto_atTop_mul_right_of_le' (G := Gᵒᵈ) _ C hf hg

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