isProbabilityMeasure — Mathlib

English

Under the given hypotheses, ℙ is a probability measure.

Русский

При данных гипотезах ℙ является вероятностной мерой.

LaTeX

$$$\\mathbb{P}\\text{ is a probability measure}$$$

Lean4

theorem isProbabilityMeasure {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) (hu : IsUniform X s ℙ μ) :
    IsProbabilityMeasure ℙ :=
  ⟨by
    have : X ⁻¹' Set.univ = Set.univ := Set.preimage_univ
    rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ, ENNReal.div_self hns hnt]⟩

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