map_symm — Mathlib

English

Dual relation to the previous: μ.map e.symm = μ.comap e; equivalence of directions under symmetry.

Русский

Двойственная связь к предыдущему: μ.map e.symm = μ.comap e; эквивалентность направлений под симметрией.

LaTeX

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

Lean4

theorem map_symm {μ : Measure α} (e : β ≃ᵐ α) : μ.map e.symm = μ.comap e := by rw [← comap_symm, symm_symm]

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