prob_add_prob_compl

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

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

English

For a measurable set s, μ(s) + μ(sᶜ) = 1.

Русский

Для измеримого множества s выполняется μ(s) + μ(sᶜ) = 1.

LaTeX

$$$\operatorname{MeasurableSet}(s) \Rightarrow \mu(s) + \mu(s^{c}) = 1$$$

Lean4

theorem prob_add_prob_compl [IsProbabilityMeasure μ] (h : MeasurableSet s) : μ s + μ sᶜ = 1 :=
  (measure_add_measure_compl h).trans measure_univ

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

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

Разделы

Аффилиация

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