Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.continuous_iff_forall_continuousMap_continuous_lintegral

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.FiniteMeasure Ω} [CompactSpace Ω],
  Continuous μs ↔ ∀ (f : C(Ω, NNReal)), Continuous fun x => ∫⁻ (ω : Ω), ↑(f ω) ∂↑(μs x)

The characterization of weak convergence of finite measures by the condition that the integrals of every continuous bounded nonnegative function are continuous.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpaceTopologicalSpaceCompactSpace