measureReal_add_measureReal_compl

English

If μ is finite and s is measurable, then μ.real s + μ.real sᶜ = μ.real univ.

Русский

Если μ конечна и s измеримо, то μ.real s + μ.real sᶜ = μ.real univ.

LaTeX

$$$ \\mu.real s + \\mu.real s^{\\complement} = \\mu.real \\mathrm{univ} $$$

Lean4

theorem measureReal_add_measureReal_compl [IsFiniteMeasure μ] (h : MeasurableSet s) :
    μ.real s + μ.real sᶜ = μ.real univ :=
  measureReal_add_measureReal_compl₀ h.nullMeasurableSet

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