tendsto_atTop_mul_right_of_le' — Mathlib

English

In a commutative group with order, for any filter l on α and any C, if the function f is bounded below by C eventually, then Tendsto (f x · g x) toTop follows from Tendsto g toTop.

Русский

В группе с порядком, при фильтре l и константе C, если f(x) ≥ C позднее, то Tendsto (f(x) g(x)) к atTop следует из Tendsto g к atTop.

LaTeX

$$$\\forall l:\\Filter\\ α,\\ \\forall f,g:\\alpha\\to G\\, (C)\\; (\\forall^\\infty x\\in l, f(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 in l, C ≤ g x) :
    Tendsto (fun x => f x * g x) l atTop :=
  .atTop_of_mul_isBoundedUnder_le (g := g⁻¹) ⟨C⁻¹, by simpa⟩ (by simpa)

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