isFiniteMeasure_of_map — Mathlib

English

IsFiniteMeasure (μ.map f) iff IsFiniteMeasure μ for AE-measurable f.

Русский

IsFiniteMeasure(μ.map f) эквивалентно IsFiniteMeasure μ для AEMeasurable f.

LaTeX

$$IsFiniteMeasure( μ.map f ) ↔ IsFiniteMeasure μ$$

Lean4

theorem isFiniteMeasure_of_map {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) [IsFiniteMeasure (μ.map f)] :
    IsFiniteMeasure μ where
  measure_univ_lt_top := by
    rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]
    exact IsFiniteMeasure.measure_univ_lt_top

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