map_iff — Mathlib

English

For a homeomorphism f, Regular(map f μ) is equivalent to Regular μ.

Русский

Для гомеоморфизма f регулярность карты сохраняется: Regular(map f μ) эквивалентна Regular μ.

LaTeX

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

Lean4

protected theorem map_iff [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] (f : α ≃ₜ β) :
    Regular (Measure.map f μ) ↔ Regular μ :=
  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

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