English
If μ is regular and f is a open embedding, then the pulled-back measure comap f μ is regular.
Русский
Если μ регулярная и f — открытое вложение, то обратное изображение по f сохраняет регулярность.
LaTeX
$$$\\text{Regular}(\\mu \\circ f)\\ $ для открытого вложения $f$.$$
Lean4
protected theorem comap' [BorelSpace α] {mβ : MeasurableSpace β} [TopologicalSpace β] [BorelSpace β] (μ : Measure β)
[Regular μ] {f : α → β} (hf : IsOpenEmbedding f) : (μ.comap f).Regular :=
by
haveI := OuterRegular.comap' μ hf.continuous hf.measurableEmbedding
haveI := IsFiniteMeasureOnCompacts.comap' μ hf.continuous hf.measurableEmbedding
exact
⟨InnerRegularWRT.comap Regular.innerRegular hf.measurableEmbedding (fun _ hU ↦ hf.isOpen_iff_image_isOpen.mp hU)
(fun _ hKrange hK ↦ hf.isInducing.isCompact_preimage' hK hKrange)⟩
