map_map_symm — Mathlib

English

For a MeasurableEquiv e and a measure ν, the two-step pushforward (ν.map e^{-1}).map e equals ν.

Русский

Для измеримого эквивалента e и меры ν последовательный перенос через e^{-1} и затем через e дает ту же меру ν.

LaTeX

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

Lean4

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

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