of_map — Mathlib

English

Let μ be a measure on α, f: α → β be AEMeasurable with respect to μ, and μ.map f be σ-finite. Then μ is σ-finite.

Русский

Пусть μ — мера на α, f: α → β — АЕ-измеримая относительно μ, и μ.map f является σ-конечной. Тогда μ является σ-конечной.

LaTeX

$$$\text{AEMeasurable}(f,\mu) \land \sigma\text{-finite}(\mu\mapsto f) \Rightarrow \sigma\text{-finite}(\mu)$$$

Lean4

theorem of_map (μ : Measure α) {f : α → β} (hf : AEMeasurable f μ) (h : SigmaFinite (μ.map f)) : SigmaFinite μ :=
  ⟨⟨⟨fun n => f ⁻¹' spanningSets (μ.map f) n, fun _ => trivial, fun n => by
        simp only [← map_apply_of_aemeasurable hf, measurableSet_spanningSets, measure_spanningSets_lt_top], by
        rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]⟩⟩⟩

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