Theorems · Theorem · measure theory

MeasureTheory.continuous_of_dominated

∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {X : Type u_6} [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → α → G}
  {bound : α → ℝ},
  (∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) μ) →
    (∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, Continuous fun x => F x a) → Continuous fun x => ∫ (a : α), F x a ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceFirstCountableTopology