Theorems · Theorem · measure theory
IntervalIntegrable.mul_continuousOn
∀ {A : Type u_7} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A},
IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => f x * g x) μ a b- Cited by
- 7 results in Mathlib
- Foundations
- Depth 220 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ContinuousOnstatement and proof · cited by 1,411
- NormedRingstatement and proof · cited by 924
- Set.uIccstatement and proof · cited by 393
- IntervalIntegrablestatement and proof · cited by 316
- measurableSet_Iocproof · cited by 65
- Set.Ioc_subset_Icc_selfproof · cited by 53
- intervalIntegrable_iffproof · cited by 29
- isCompact_uIccproof · cited by 17
- MeasureTheory.IntegrableOn.mul_continuousOn_of_subsetproof · cited by 2
Cited by7
Results whose statement or proof uses this declaration.
- intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_rightproof · cited by 2
- IntervalIntegrable.mul_constproof · cited by 2
- intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_rightproof · cited by 2
- hasSum_two_pi_I_cauchyPowerSeries_integralproof · cited by 2
- Complex.betaIntegral_convergent_leftproof · cited by 1
- CircleIntegrable.mul_continuousOnproof · cited by 1
- AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mulproof · cited by 1