simp
a : ℝ
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Iic a)
hg_int : IntegrableOn g (Set.Iic a)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Iic a)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Iic a)
⊢ MeasurableSet (Set.Iic a)
no goals