English
A measure pushed along a homeomorphism preserves outer regularity.
Русский
Обусловленное отображением меры через гомоморфизм сохраняет внешнюю регулярность.
LaTeX
$$$map\ f\ μ\text{ OuterRegular}$, если $μ\text{ OuterRegular}$ и $f$ - гомеоморфизм.$$
Lean4
protected theorem map [OpensMeasurableSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β)
(μ : Measure α) [OuterRegular μ] : (Measure.map f μ).OuterRegular :=
by
refine ⟨fun A hA r hr => ?_⟩
rw [map_apply f.measurable hA, ← f.image_symm] at hr
rcases Set.exists_isOpen_lt_of_lt _ r hr with ⟨U, hAU, hUo, hU⟩
have : IsOpen (f.symm ⁻¹' U) := hUo.preimage f.symm.continuous
refine ⟨f.symm ⁻¹' U, image_subset_iff.1 hAU, this, ?_⟩
rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]
