exact Continuous.sub hφ.continuous continuous_const
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => φ x - φ 0
no goals