toMeasure_apply_eq_toOuterMeasure

English

For a PMF p (with a measurable singleton class), the measure of any set s equals the outer measure of s, i.e., p.toMeasure(s) = p.toOuterMeasure(s).

Русский

Для PMF p (с измеримой одиничной полнотой) мера множества s равна внешней мере: p.toMeasure(s) = p.toOuterMeasure(s).

LaTeX

$$$\\forall s:\\ Set(\\alpha),\\; p.toMeasure(s) = p.toOuterMeasure(s)$$$

Lean4

theorem toMeasure_apply_eq_toOuterMeasure (s : Set α) : p.toMeasure s = p.toOuterMeasure s :=
  by
  have hs := (p.support_countable.mono s.inter_subset_right).measurableSet
  rw [← restrict_toMeasure_support, Measure.restrict_apply' p.support_countable.measurableSet,
    p.toMeasure_apply_eq_toOuterMeasure_apply hs, toOuterMeasure_apply_inter_support]

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