restrict_toMeasure_support — Mathlib

English

For a PMF p, restricting its associated measure to its support leaves the measure unchanged; i.e., p.toMeasure.restrict(p.support) = p.toMeasure.

Русский

Для PMF p ограничение связанной с p меры до опоры p не меняет меру; то есть p.toMeasure.restrict(p.support) = p.toMeasure.

LaTeX

$$$ p.toMeasure \\restriction p.support = p.toMeasure $$$

Lean4

@[simp]
theorem restrict_toMeasure_support : p.toMeasure.restrict p.support = p.toMeasure :=
  by
  ext s hs
  rw [Measure.restrict_apply hs, p.toMeasure_apply_inter_support hs]

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