map — Mathlib

English

Push-forward of a measure with IsFiniteMeasureOnCompacts by a homeomorphism preserves the property on compact sets.

Русский

Перенос меры по отображению-гомеоморфизму сохраняет свойство конечности на компакта.

LaTeX

$$$\\text{IsFiniteMeasureOnCompacts}(\\\\mu) \\Rightarrow \\text{IsFiniteMeasureOnCompacts}(\\\\mu.map f)$$$

Lean4

protected theorem map (μ : Measure α) [IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β) :
    IsFiniteMeasureOnCompacts (μ.map f) := by
  refine ⟨fun K hK ↦ ?_⟩
  rw [← f.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]
  exact IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)

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