measure_compl₀ — Mathlib

English

If s is null-measurable and μ s ≠ ∞, then μ sᶜ = μ univ − μ s.

Русский

Если s нулемеримо измеримо и μ(s) ≠ ∞, то μ sᶜ = μ(полное множество) − μ(s).

LaTeX

$$$$ \\mu(s^{\\mathrm{c}}) = \\mu(\\mathsf{univ}) - \\mu(s). $$$$

Lean4

theorem measure_compl₀ (h : NullMeasurableSet s μ) (hs : μ s ≠ ∞) : μ sᶜ = μ Set.univ - μ s := by
  rw [← measure_add_measure_compl₀ h, ENNReal.add_sub_cancel_left hs]

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