toMeasure_apply_eq_zero_iff — Mathlib

English

For PMF p and s, p.toMeasure s = 0 iff Disjoint(p.support, s).

Русский

Для PMF p и множества s: p.toMeasure s = 0 тогда и только тогда, когда p.support дисjoint с s.

LaTeX

$$$ p.toMeasure s = 0 \iff \mathrm{Disjoint}(p.\mathrm{support}, s) $$$

Lean4

theorem toMeasure_apply_eq_zero_iff (hs : MeasurableSet s) : p.toMeasure s = 0 ↔ Disjoint p.support s := by
  rw [p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_eq_zero_iff]

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