sigmaFinite — Mathlib

English

If f is measure-preserving from μa to μb and μb is σ-finite, then μa is σ-finite.

Русский

Если f сохраняет меру от μa к μb и μbётся σ-конечна, то μa тоже σ-конечна.

LaTeX

$$$\text{MeasurePreserving } f\, μ_a\, μ_b \rightarrow [\SigmaFinite\, μ_b] \rightarrow \SigmaFinite\, μ_a$$$

Lean4

protected theorem sigmaFinite {f : α → β} (hf : MeasurePreserving f μa μb) [SigmaFinite μb] : SigmaFinite μa :=
  SigmaFinite.of_map μa hf.aemeasurable (by rwa [hf.map_eq])

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