simp [isClosed_Icc, isPreconnected_Icc, hab]
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_int : IntegrableOn g (Set.Icc a b)
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ (Set.Icc a b)] g
h_int : IntegrableOn (fun x => f x * g x) (Set.Icc a b)
⊢ IsClosed (Set.Icc a b)
no goals