English
If f is an open embedding, then the comap measure μ.comap f inherits inner regularity from μ; i.e., (μ.comap f).InnerRegular holds given μ.InnerRegular.
Русский
Если f есть открытое вложение, то мера, полученная обратным образом через f, наследует внутреннюю регулярность от μ.
LaTeX
$$$[BorelSpace\\ α] [TopologicalSpace β] [BorelSpace β](μ : Measure β)[H: InnerRegular μ]\\; \\text{IsOpenEmbedding } f \\Rightarrow (Measure.comap f μ).InnerRegular$$$
Lean4
protected theorem comap' [BorelSpace α] {mβ : MeasurableSpace β} [TopologicalSpace β] [BorelSpace β] (μ : Measure β)
[H : InnerRegular μ] {f : α → β} (hf : IsOpenEmbedding f) : (μ.comap f).InnerRegular where
innerRegular :=
H.innerRegular.comap hf.measurableEmbedding (fun _ hU ↦ hf.measurableEmbedding.measurableSet_image' hU)
(fun _ hKrange hK ↦ hf.isInducing.isCompact_preimage' hK hKrange)
