symm_symm — Mathlib

English

The map γ ↦ γ^{symm} is a bijection between Path x y and Path y x; its inverse is itself.

Русский

Оперaция симмм между путями задаёт биекцию между путями из x в y и из y в x; обратная — та же операция.

LaTeX

$$$\\text{Bijective}(\\text{Path.symm})\\quad\\text{with inverse }\\text{Path.symm}$$$

Lean4

@[simp]
theorem symm_symm (γ : Path x y) : γ.symm.symm = γ := by
  ext t
  change γ (σ (σ t)) = γ t
  rw [unitInterval.symm_symm]

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