map — Mathlib

English

If α ≃ₜ β is a homeomorphism and μ is inner regular with respect to open/closed, then the pushforward measure under the homeomorphism is inner regular as well.

Русский

Если имеется гомеоморфизм f между пространствами, и μ — внутренняя регулярность, то образ меры под f сохраняет внутреннюю регулярность.

LaTeX

$$$[BorelSpace\\ α][MeasurableSpace\\ β][TopologicalSpace\\ β][BorelSpace\\ β][InnerRegular μ]\\; (f : α \\to β)\\Rightarrow InnerRegular (Measure.map f μ)$$$

Lean4

protected theorem map [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] [InnerRegular μ]
    (f : α ≃ₜ β) : (Measure.map f μ).InnerRegular :=
  InnerRegular.map_of_continuous f.continuous

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