sfinite_of_isFiniteMeasure — Mathlib

English

If every finite μ has a Lebesgue decomposition w.r.t. ν, then any s-finite μ also does.

Русский

Если для каждого конечного μ существует разложение Лебеса по ν, то и для любой s-финитной μ существует разложение Лебеса по ν.

LaTeX

$$$$ [SFinite(\\mu)] \\Rightarrow (\\forall \\mu,\\text{if } \\mu \\text{ finite then } HaveLebesgueDecomposition(\\mu, \\nu)) $$$$

Lean4

/-- If any finite measure has a Lebesgue decomposition with respect to `ν`,
then the same is true for any s-finite measure. -/
theorem sfinite_of_isFiniteMeasure [SFinite μ]
    (_h : ∀ (μ : Measure α) [IsFiniteMeasure μ], HaveLebesgueDecomposition μ ν) : HaveLebesgueDecomposition μ ν :=
  sum_sfiniteSeq μ ▸ sum_left _

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