sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero

English

If μ restricted to the complement of μ.sigmaFiniteSet is zero, then μ is sigma-finite.

Русский

Если μ на дополнении μ.sigmaFiniteSet равно нулю, то μ сигма-финитна.

LaTeX

$$$$\text{If } μ(\mu.sigmaFiniteSet^c)=0 \Rightarrow \text{SigmaFinite}(μ).$$$$

Lean4

theorem sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero (h : μ μ.sigmaFiniteSetᶜ = 0) : SigmaFinite μ :=
  by
  rw [← Measure.restrict_add_restrict_compl (μ := μ) (measurableSet_sigmaFiniteSet (μ := μ)),
    Measure.restrict_eq_zero.mpr h, add_zero]
  infer_instance

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