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

theorem continuous_integral_finiteMeasure {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (f : BoundedContinuousFunction α ℝ) : Continuous fun (μ : MeasureTheory.FiniteMeasure α) => ∫ (x : α), f x ∂↑μ

theorem continuous_integral_probabilityMeasure {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] (f : BoundedContinuousFunction α ℝ) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure α) => ∫ (x : α), f x ∂↑μ

noncomputable def indicatorBCF {α : Type u_1} [TopologicalSpace α] {s : Set α} (s_clopen : IsClopen s) : BoundedContinuousFunction α ℝ

The indicator function of a clopen set, as a bounded continuous function.

Equations

• indicatorBCF s_clopen = { toFun := s.indicator fun (x : α) => 1, continuous_toFun := ⋯, map_bounded' := ⋯ }

@[simp]

theorem indicatorBCF_apply {α : Type u_1} [TopologicalSpace α] {s : Set α} (s_clopen : IsClopen s) (x : α) : (indicatorBCF s_clopen) x = s.indicator (fun (x : α) => 1) x

theorem lintegral_indicatorBCF {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) {s : Set α} (s_clopen : IsClopen s) (s_mble : MeasurableSet s) : ∫⁻ (x : α), ENNReal.ofReal ((indicatorBCF s_clopen) x) ∂μ = μ s

theorem integral_indicatorBCF {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) {s : Set α} (s_clopen : IsClopen s) (s_mble : MeasurableSet s) : ∫ (x : α), (indicatorBCF s_clopen) x ∂μ = (μ s).toReal