map_symm_map — Mathlib

English

For a MeasurableEquiv e, mapping by e and then by e^{-1} returns the original measure: (μ.map e).map e^{-1} = μ.

Русский

С учетом обратного отображения, перенос меры по e и затем по e^{-1} возвращает исходную меру: (μ.map e).map e^{-1} = μ.

LaTeX

$$$$\\forall \\mu:\\mathrm{Measure}\\,\\alpha,\\forall e:\\alpha \\simeq\\beta,\\; (\\mu.map e).map e^{-1} = \\mu.$$$$

Lean4

@[simp]
theorem map_symm_map (e : α ≃ᵐ β) : (μ.map e).map e.symm = μ := by simp [map_map e.symm.measurable e.measurable]

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