measure_add_measure_compl

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measure_add_measure_compl

English

For a measurable set s, μ(s) + μ(s^c) = μ(univ).

Русский

Для измеримого множества s имеем μ(s) + μ(s^c) = μ(всё множество).

LaTeX

$$$$\\forall s:\\mathrm Set,\\; \\mathrm{MeasurableSet}(s) \\rightarrow \\mu(s) + \\mu(s^c) = \\mu(\\text{univ}).$$$$

Lean4

theorem measure_add_measure_compl (h : MeasurableSet s) : μ s + μ sᶜ = μ univ :=
  measure_add_measure_compl₀ h.nullMeasurableSet

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru