mul — Mathlib

English

If f and g are bounded along l, then f · g is bounded along l.

Русский

Если f и g ограничены вдоль l, то f · g ограничен вдоль l.

LaTeX

$$$\\mathrm{BoundedAtFilter}(l,f) \\land \\mathrm{BoundedAtFilter}(l,g) \\Rightarrow \\mathrm{BoundedAtFilter}(l, f \\cdot g)$$$

Lean4

nonrec theorem mul [SeminormedRing β] {l : Filter α} {f g : α → β} (hf : BoundedAtFilter l f)
    (hg : BoundedAtFilter l g) : BoundedAtFilter l (f * g) :=
  by
  refine (hf.mul hg).trans ?_
  convert Asymptotics.isBigO_refl (E := ℝ) _ l
  simp

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