add — Mathlib

English

If two functions f and f' both vanish at cusp c with order k, then their sum f + f' also vanishes at c with order k.

Русский

Если две функции f и f', имеющие нулевой порядок k в точке cusp c, складываются, то их сумма f + f' также имеет нулевой порядок k в этой точке.

LaTeX

$$$\mathrm{IsZeroAt}(c,f,k) \land \mathrm{IsZeroAt}(c,g,k) \Rightarrow \mathrm{IsZeroAt}(c,f+g,k)$$$

Lean4

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

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