measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite

English

Equivalent formulation: μ is sigma-finite iff μ(μ.sigmaFiniteSet)ᶜ = 0.

Русский

Эквивалентная формулировка: μ сигма-финитна тогда и только тогда, когда μ(μ.sigmaFiniteSet)ᶜ = 0.

LaTeX

$$$$\mu(\mu.sigmaFiniteSet)^{c} = 0 \iff \SigmaFinite(μ).$$$$

Lean4

/-- An s-finite measure `μ` is sigma-finite iff `μ μ.sigmaFiniteSetᶜ = 0`. -/
theorem measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite (μ : Measure α) :
    μ μ.sigmaFiniteSetᶜ = 0 ↔ SigmaFinite μ :=
  ⟨sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero, fun _ ↦ measure_compl_sigmaFiniteSet μ⟩

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