exact exists_mul_eq_setInterval_Icc_of_continuousOn hab hf_cont hg_cont hg_nonneg
a b : ℝ
hab : a ≤ b
f g : ℝ → ℝ
μ : Measure ℝ
inst✝¹ : NoAtoms μ
inst✝ : IsLocallyFiniteMeasure μ
hf_cont : ContinuousOn f (Set.Icc a b)
hg_cont : ContinuousOn g (Set.Icc a b)
hg_nonneg : ∀ x ∈ Set.Icc a b, 0 ≤ g x
⊢ ∃ c ∈ Set.Icc a b, ∫ (x : ℝ) in Set.Icc a b, f x * g x ∂μ = f c * ∫ (x : ℝ) in Set.Icc a b, g x ∂μ
no goals