measureReal_add_measureReal_compl₀

English

For finite μ, and NullMeasurable s, μ.real s + μ.real sᶜ = μ.real univ.

Русский

При конечной мере μ и NullMeasurable 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 μ] (hs : NullMeasurableSet s μ) :
    μ.real s + μ.real sᶜ = μ.real univ := by rw [← measureReal_union₀' hs aedisjoint_compl_right, union_compl_self]

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