Theorems · Theorem · complex analysis

Function.Periodic.cuspFunction_add

∀ {h : ℝ} {f g : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    ContinuousAt (Function.Periodic.cuspFunction h g) 0 →
      Function.Periodic.cuspFunction h (f + g) = Function.Periodic.cuspFunction h f + Function.Periodic.cuspFunction h g

Defined in

Mathlib.Analysis.Complex.Periodic

Cited by

2 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound