Theorems · Theorem · measure theory

intervalIntegral.continuous_parametric_primitive_of_continuous

∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : X → ℝ → E} {a₀ : ℝ}, Continuous (Function.uncurry f) → Continuous fun p => ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ

Defined in

Mathlib.MeasureTheory.Integral.DominatedConvergence

Cited by

1 results in Mathlib

Foundations

Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceMeasureTheory.NullSingletonClassMeasureTheory.IsLocallyFiniteMeasure