add — Mathlib

English

The sum of two cusp-bounded objects with the same cusp remains cusp-bounded at that cusp.

Русский

Сумма двух ограниченных в cusp объектов остаётся ограниченной в этом cusp.

LaTeX

$$If f and f' are bounded at c with weight k, then f+f' is bounded at c with weight k.$$

Lean4

theorem add {f' : ℍ → ℂ} (hf : IsBoundedAt c f k) (hf' : IsBoundedAt c f' k) : IsBoundedAt c (f + f') k := fun g hg ↦ by
  simpa using (hf g hg).add (hf' g hg)

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