The measure of a connected component of a space depends continuously on a finite measure

theorem continuous_finiteMeasure_apply_of_isClopen {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (s_clopen : IsClopen s) : Continuous fun (μ : MeasureTheory.FiniteMeasure α) => (↑μ).real s

The measure of any connected component depends continuously on the FiniteMeasure.

theorem continuous_probabilityMeasure_apply_of_isClopen {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α} (s_clopen : IsClopen s) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure α) => (↑μ).real s

The probability of any connected component depends continuously on the ProbabilityMeasure.