prob_compl_eq_one_sub — Mathlib

English

For measurable s, μ sᶜ = 1 - μ s.

Русский

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

LaTeX

$$$\text{MeasurableSet}(s) \Rightarrow \mu(s^{c}) = 1 - \mu(s)$$$

Lean4

/-- Note that this is not quite as useful as it looks because the measure takes values in `ℝ≥0∞`.
Thus the subtraction appearing is the truncated subtraction of `ℝ≥0∞`, rather than the
better-behaved subtraction of `ℝ`. -/
theorem prob_compl_eq_one_sub (hs : MeasurableSet s) : μ sᶜ = 1 - μ s :=
  prob_compl_eq_one_sub₀ hs.nullMeasurableSet

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