map_apply_map_symm_eq

Mathlib.Algebra.FreeMonoid.Basic

URI: https://scilib.ai/kg/mathlib#FreeMonoid.map_apply_map_symm_eq

English

Similarly, (map e) ((map e.symm) x) = x for x ∈ FreeMonoid β and equivalence e: α ≃ β.

Русский

Аналогично, (map e) ((map e.symm) x) = x для x ∈ FreeMonoid β и эквивалентности e: α ≃ β.

LaTeX

$$$ (map\ e)\ ((map\ e.symm)\ x) = x $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru