prob_compl_eq_one_sub₀ — Mathlib

English

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

Русский

Для нуль-измеримого s: μ(sᶜ) = 1 - μ(s).

LaTeX

$$$\text{NullMeasurableSet}(s,\mu) \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₀ (h : NullMeasurableSet s μ) : μ sᶜ = 1 - μ s := by
  rw [measure_compl₀ h (measure_ne_top _ _), measure_univ]

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