boundedAtFilter — 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+g)$$$

Lean4

theorem boundedAtFilter [SeminormedAddGroup β] {l : Filter α} {f : α → β} (hf : ZeroAtFilter l f) :
    BoundedAtFilter l f :=
  ((Asymptotics.isLittleO_one_iff _).mpr hf).isBigO

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