map_iff — Mathlib

English

For a homeomorphism f, inner regularity is preserved by map f if and only if μ is inner regular on the original space; i.e., InnerRegular (map f μ) ↔ InnerRegular μ.

Русский

Для гомеоморфизма f внутреннюю регулярность сохраняет отображение мер, и наоборот: InnerRegular (map f μ) ↔ InnerRegular μ.

LaTeX

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

Lean4

protected theorem map_iff [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) :
    InnerRegular (Measure.map f μ) ↔ InnerRegular μ :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
  convert h.map f.symm
  rw [map_map f.symm.continuous.measurable f.continuous.measurable]
  simp

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