haveLebesgueDecomposition_of_sigmaFinite

English

If μ is sigma-finite, then every signed measure s has a Lebesgue decomposition with respect to μ.

Русский

Если μ — сигма-ограниченная, то любая знаковая мера s имеет разложение Лебега относительно μ.

LaTeX

$$$[\text{SigmaFinite }\mu] \Rightarrow s.HaveLebesgueDecomposition\mu$$$

Lean4

instance (priority := 100) haveLebesgueDecomposition_of_sigmaFinite (s : SignedMeasure α) (μ : Measure α)
    [SigmaFinite μ] : s.HaveLebesgueDecomposition μ
    where
  posPart := inferInstance
  negPart := inferInstance

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