comap — Mathlib

English

If f is a homeomorphism, then the inner regularity of μ is equivalent to the inner regularity of the comapped measure under f; i.e., comap f preserves InnerRegular.

Русский

Если f — гомеоморфизм, то внутренняя регулярность меры μ эквивалентна внутренней регулярности меры, полученной посредством comap f; т.е. comap f сохраняет InnerRegular.

LaTeX

$$$[BorelSpace\\ α][BorelSpace β] (f : α \\to β)\\; (μ.InnerRegular) \\Rightarrow (μ.comap f).InnerRegular$$

Lean4

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

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