comap_symm — Mathlib

English

For a measurable equivalence e, μ.comap e.symm = μ.map e; switching the direction preserves the relation between comap and map.

Русский

Для измеримого эквивалента e, μ.comap e.symm = μ.map e; направление отображения может быть поменяно.

LaTeX

$$$\\mu.\\mathrm{comap}\\ e^{\\mathrm{symm}} = \\mu.\\mathrm{map}\\ e$$$

Lean4

theorem comap_symm {μ : Measure α} (e : α ≃ᵐ β) : μ.comap e.symm = μ.map e :=
  by
  ext s hs
  rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm]
  exact fun t ht ↦ e.symm.measurableSet_image.mpr ht

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