comap — Mathlib

English

Under a homeomorphism, the comap of an outer regular measure remains outer regular.

Русский

При гамоморфизме образ массы сохраняется внешняя регулярность.

LaTeX

$$$[BorelSpace]\; μ, f: X\simeq_t Y \Rightarrow OuterRegular(\mu) \Rightarrow OuterRegular(\text{comap } f\, μ)$$$

Lean4

protected theorem comap [BorelSpace α] {mβ : MeasurableSpace β} [TopologicalSpace β] [BorelSpace β] (μ : Measure β)
    [OuterRegular μ] (f : α ≃ₜ β) : (μ.comap f).OuterRegular :=
  OuterRegular.comap' μ f.continuous f.measurableEmbedding

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