toMeasure_apply_inter_support — Mathlib

English

Let p be a probability mass function on a measurable space, and let s be a measurable set. Then the measure associated to p assigns the same value to s as to s intersect the support of p; i.e., p.toMeasure(s ∩ supp(p)) = p.toMeasure(s).

Русский

Пусть p — распределение массы вероятностей на измеримом пространстве, и пусть s — измеримое множество. Тогда мера, соответствующая p, равна между s и s ∩ supp(p); то есть p.toMeasure(s ∩ supp(p)) = p.toMeasure(s).

LaTeX

$$$ p.toMeasure(s \\cap p.support) = p.toMeasure(s) $$$

Lean4

@[simp]
theorem toMeasure_apply_inter_support (hs : MeasurableSet s) : p.toMeasure (s ∩ p.support) = p.toMeasure s :=
  (measure_mono s.inter_subset_left).antisymm (p.toMeasure_mono hs (refl _))

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