measurableSet_isProbabilityMeasure

English

The set of all probability measures on Ω is a measurable subset of the space of all measures on Ω.

Русский

Множество всех вероятностных мер на Ω является измеримым подмножеством пространства всех мер на Ω.

LaTeX

$$$\\text{MeasurableSet}\\;\\{\\mu : \\text{Measure } \\Omega \\mid \\text{IsProbabilityMeasure } \\mu\\}$$$

Lean4

theorem measurableSet_isProbabilityMeasure : MeasurableSet {μ : Measure Ω | IsProbabilityMeasure μ} :=
  by
  suffices {μ : Measure Ω | IsProbabilityMeasure μ} = (fun μ => μ univ) ⁻¹' { 1 }
    by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ (measurableSet_singleton 1)
  ext _
  apply isProbabilityMeasure_iff

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