sigmaFinite_map — Mathlib

English

If f is a measurable equivalence and μ is σ-finite, then μ.map f is σ-finite.

Русский

Пусть f — измеримое эквивалентное отображение и μ — сигма-конечна; тогда μ.map f сигма-конечна.

LaTeX

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

Lean4

theorem _root_.MeasurableEquiv.sigmaFinite_map (f : α ≃ᵐ β) [SigmaFinite μ] : SigmaFinite (μ.map f) :=
  f.measurableEmbedding.sigmaFinite_map

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