tendsto_atBot_mul_left_of_ge — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem tendsto_atBot_mul_left_of_ge (C : G) (hf : ∀ x, 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

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