isFiniteMeasure_map — Mathlib

English

If μ is finite and f is AE-measurable, then μ.map f is finite.

Русский

Если μ конечна и f AE-измеримо, то μ.map f конечна.

LaTeX

$$IsFiniteMeasure( μ.map f )$$

Lean4

@[instance]
theorem isFiniteMeasure_map {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → β) :
    IsFiniteMeasure (μ.map f) := by
  by_cases hf : AEMeasurable f μ
  · constructor
    rw [map_apply_of_aemeasurable hf MeasurableSet.univ]
    exact measure_lt_top μ _
  · rw [map_of_not_aemeasurable hf]
    exact MeasureTheory.isFiniteMeasureZero

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