measureReal_compl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem measureReal_compl [IsFiniteMeasure μ] (h₁ : MeasurableSet s) : μ.real sᶜ = μ.real univ - μ.real s :=
  by
  rw [compl_eq_univ_diff]
  exact measureReal_diff (subset_univ s) h₁

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