English
If μ is inner regular, then the pushforward measure under a homeomorphism f is also inner regular (under appropriate topological hypotheses such as Borel spaces). In particular, InnerRegular μ implies InnerRegular (map f μ).
Русский
Если μ внутренняя регулярность, то под действием гомеоморфизма f образ-меры μ переносит свою внутреннюю регулярность: InnerRegular μ ⇒ InnerRegular (map f μ).
LaTeX
$$$[BorelSpace\\ α]\\; [MeasurableSpace\\ β]\\; [TopologicalSpace\\ β]\\; [BorelSpace\\ β]\\; [μ.InnerRegular] \\Rightarrow InnerRegular (Measure.map f μ)$$$
Lean4
/-- The measure of a measurable set is the supremum of the measures of compact sets it contains. -/
theorem _root_.MeasurableSet.measure_eq_iSup_isCompact ⦃U : Set α⦄ (hU : MeasurableSet U) (μ : Measure α)
[InnerRegular μ] : μ U = ⨆ (K : Set α) (_ : K ⊆ U) (_ : IsCompact K), μ K :=
InnerRegular.innerRegular.measure_eq_iSup hU
