IsProbabilityMeasure_comap_equiv — Mathlib

English

If f is a measurable equivalence, then μ.comap f is a probability measure.

Русский

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

LaTeX

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

Lean4

instance IsProbabilityMeasure_comap_equiv (f : β ≃ᵐ α) : IsProbabilityMeasure (μ.comap f) := by
  rw [← MeasurableEquiv.map_symm]; exact isProbabilityMeasure_map f.symm.measurable.aemeasurable

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