map — Mathlib

English

If μ is regular and f is a homeomorphism, then the pushforward measure map f μ is regular.

Русский

Если μ регулярная, и f — гомеоморфизм, то образующая мера map f μ также регулярна.

LaTeX

$$$\\text{Regular}(\\mu) \\Rightarrow \\text{Regular}(\\text{map } f \\mu).$$$

Lean4

protected theorem map [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [Regular μ] (f : α ≃ₜ β) :
    (Measure.map f μ).Regular := by
  haveI := OuterRegular.map f μ
  haveI := IsFiniteMeasureOnCompacts.map μ f
  exact
    ⟨Regular.innerRegular.map' f.toMeasurableEquiv (fun U hU => hU.preimage f.continuous)
        (fun K hK => hK.image f.continuous)⟩

Похожие утверждения