apply integrable_mul_continuous <;> assumption
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : Continuous f
hg : IsBump g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (g * f)
no goals