map_symm — Mathlib

English

Mapping a path and then taking its symmetric image is the same as taking the symmetric image first and then mapping.

Русский

Пусть путь отображается, затем берётся симметрия; эквивалентно сначала взять симметрию, затем отобразить.

LaTeX

$$$(\gamma.map h).symm = \gamma.symm.map h$$$

Lean4

@[simp]
theorem map_symm (γ : Path x y) {f : X → Y} (h : Continuous f) : (γ.map h).symm = γ.symm.map h :=
  rfl

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