isProbabilityMeasure_comap_down — Mathlib

English

The comap under ULift.down of a probability measure is a probability measure.

Русский

Обратное изображение под ULift.down вероятностной меры — вероятность мера.

LaTeX

$$$\mathrm{IsProbabilityMeasure}(\mathrm{comap}\ {\mathrm{ULift}}\mathrm{down}\ mu)$$$

Lean4

instance isProbabilityMeasure_comap_down : IsProbabilityMeasure (μ.comap ULift.down) :=
  MeasurableEquiv.ulift.measurableEmbedding.isProbabilityMeasure_comap <|
    ae_of_all _ <| by simp [Function.Surjective.range_eq <| EquivLike.surjective _]

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