. exact Continuous.mul hf.continuous hg
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous (f * g)

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)