isProbabilityMeasure_comap — Mathlib

English

If f is a MeasurableEmbedding, then IsProbabilityMeasure comap f μ.

Русский

Если f — измеримое вложение, то μ.comap f — вероятностная мера.

LaTeX

$$$\text{MeasurableEmbedding}(f) \Rightarrow \mathrm{IsProbabilityMeasure}(\mu\ comap f)$$$

Lean4

protected theorem _root_.MeasurableEmbedding.isProbabilityMeasure_comap (hf : MeasurableEmbedding f)
    (hf' : ∀ᵐ a ∂μ, a ∈ range f) : IsProbabilityMeasure (μ.comap f) :=
  isProbabilityMeasure_comap hf.injective hf' hf.measurableSet_image'

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