Inner regularity under almost everywhere continuous maps #
A measurable map that is continuous on a measurable set of full measure sends an inner regular measure to an inner regular measure. Global continuity is unnecessary: compact approximation can be performed inside the set where the map is continuous. This applies, for example, to spectral character assignments whose exceptional set has measure zero.
theorem
TauCeti.innerRegular_map_of_continuousOn
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[TopologicalSpace α]
[MeasurableSpace β]
[TopologicalSpace β]
{μ : MeasureTheory.Measure α}
[μ.InnerRegular]
{f : α → β}
{s : Set α}
(hf : Measurable f)
(hs : MeasurableSet s)
(hcont : ContinuousOn f s)
(hmem : ∀ᵐ (x : α) ∂μ, x ∈ s)
:
A measurable map continuous on a measurable set of full measure preserves inner regularity. No separation, countability or finiteness assumption is required.