tendsto_atTop_mul_right_of_le — Mathlib

English

In a group with order, if g x ≥ C eventually and f tends to atTop, then x ↦ f(x) g(x) tends to atTop.

Русский

В группе с порядком, если g(x) ≥ C позднее и f стремится к atTop, тогда 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_atTop_mul_right_of_le (C : G) (hf : Tendsto f l atTop) (hg : ∀ x, C ≤ g x) :
    Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mul_right_of_le' l C hf (univ_mem' hg)

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