add — Mathlib

English

In the BoundedAtFilter context, the sum of two bounded functions is bounded.

Русский

В контексте BoundedAtFilter сумма двух ограниченных функций ограничена.

LaTeX

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

Lean4

nonrec theorem add [SeminormedAddCommGroup β] {l : Filter α} {f g : α → β} (hf : BoundedAtFilter l f)
    (hg : BoundedAtFilter l g) : BoundedAtFilter l (f + g) := by simpa using hf.add hg

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