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 _))