map_symm_apply_map_eq — Mathlib

English

For any x ∈ FreeMonoid α and any equivalence e: α ≃ β, applying map with e and then with e.symm yields the original x: (map e.symm) ((map e) x) = x.

Русский

Для любого x ∈ FreeMonoid α и эквиваленты e: α ≃ β последовательное применение map e и затем map e.symm возвращает исходный x.

LaTeX

$$$ (map\ e^{-1})\ ((map\ e)\ x) = x $$$

Lean4

@[to_additive (attr := simp)]
theorem map_symm_apply_map_eq {x : FreeMonoid α} (e : α ≃ β) : (map ⇑e.symm) ((map ⇑e) x) = x := by simp [map_map]

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