Theorems · Theorem · measure theory

MeasureTheory.ProbabilityMeasure.continuous_testAgainstNN_eval

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (f : BoundedContinuousFunction Ω NNReal), Continuous fun μ => μ.toFiniteMeasure.testAgainstNN f

Integration of (nonnegative bounded continuous) test functions against Borel probability measures depends continuously on the measure.

Defined in

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceOpensMeasurableSpace