English
If f is a measurable embedding and μ is σ-finite, then μ.map f is σ-finite.
Русский
Пусть f — измеримое вложение и μ — сигма-конечна; тогда μ.map f сигма-конечна.
LaTeX
$$$\text{MeasurableEmbedding}(f) \land \sigma\text{-finite}(\mu) \Rightarrow \sigma\text{-finite}(\mu\mapsto f)$$$
Lean4
theorem _root_.MeasurableEmbedding.sigmaFinite_map {f : α → β} (hf : MeasurableEmbedding f) [SigmaFinite μ] :
SigmaFinite (μ.map f) :=
by
refine ⟨fun n ↦ f '' (spanningSets μ n) ∪ (Set.range f)ᶜ, by simp, fun n ↦ ?_, ?_⟩
· rw [hf.map_apply, Set.preimage_union]
simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
Set.preimage_image_eq _ hf.injective]
exact measure_spanningSets_lt_top μ n
· rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets, Set.image_univ, Set.union_compl_self]
