English
If μ is an open-positive measure on Z and f:X→Z is an open embedding, then the pullback measure μ.comap f on X is open-positive.
Русский
Если μ — открыто-положительная мера на Z и f: X → Z — открыто вложение, то мера-обратный образ μ.comap f на X является открыто-положительной.
LaTeX
$$$\\forall μ:\\ Measure Z\\,[IsOpenPosMeasure μ]\\; {f:X→Z}\\; (\\text{IsOpenEmbedding } f)\\Rightarrow (μ.comap f)\\ IsOpenPosMeasure.$$$
Lean4
theorem _root_.Continuous.isOpenPosMeasure_map [OpensMeasurableSpace X] {Z : Type*} [TopologicalSpace Z]
[MeasurableSpace Z] [BorelSpace Z] {f : X → Z} (hf : Continuous f) (hf_surj : Function.Surjective f) :
(Measure.map f μ).IsOpenPosMeasure := by
refine ⟨fun U hUo hUne => ?_⟩
rw [Measure.map_apply hf.measurable hUo.measurableSet]
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)
