measure_add_measure_compl₀ — Mathlib

English

For a set s that is null-measurable, μ(s) + μ(s^c) = μ(univ).

Русский

Для множества s, которое нулево измеримо, выполняется μ(s) + μ(s^c) = μ(полнота).

LaTeX

$$$\mathrm{NullMeasurableSet}(s,\mu) \Rightarrow \mu(s) + \mu(s^c) = \mu(\mathrm{univ}).$$$

Lean4

theorem measure_add_measure_compl₀ {s : Set α} (hs : NullMeasurableSet s μ) : μ s + μ sᶜ = μ univ := by
  rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]

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