English
Pullback of a regular measure along a continuous measurable embedding maintains outer regularity.
Русский
Обратное образ меры по непрерывному измеримому вложению сохраняет внешнюю регулярность.
LaTeX
$$$outerRegular( f^{-1}•μ )$ при $f$ непрерывно и измеримо вложение, если $μ$ внешний Регулярен.$$
Lean4
theorem comap' {mβ : MeasurableSpace β} [TopologicalSpace β] (μ : Measure β) [OuterRegular μ] {f : α → β}
(f_cont : Continuous f) (f_me : MeasurableEmbedding f) : (μ.comap f).OuterRegular where
outerRegular A hA r
hr := by
rw [f_me.comap_apply] at hr
obtain ⟨U, hUA, Uopen, hμU⟩ := OuterRegular.outerRegular (f_me.measurableSet_image' hA) r hr
refine ⟨f ⁻¹' U, by rwa [Superset, ← image_subset_iff], Uopen.preimage f_cont, ?_⟩
rw [f_me.comap_apply]
exact (measure_mono (image_preimage_subset _ _)).trans_lt hμU
