prob_compl_le_one_sub_of_le_prob — Mathlib

English

If p ≤ μ(s) for a measurable set s, then μ(s^c) ≤ 1 - p, given μ is zero-or-probability.

Русский

Пусть p ≤ μ(s) для измеримого множества s; тогда μ(s^c) ≤ 1 - p, если μ — нулевая или вероятностная мера.

LaTeX

$$$p \le \mu(s) \implies \mu(s^c) \le 1 - p$$$

Lean4

theorem prob_compl_le_one_sub_of_le_prob {p : ℝ≥0∞} (hμs : p ≤ μ s) (s_mble : MeasurableSet s) : μ sᶜ ≤ 1 - p :=
  by
  rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
  · simp
  · simpa [prob_compl_eq_one_sub s_mble] using tsub_le_tsub_left hμs 1

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