symm_symm — Mathlib

English

Re-applying the symmetry operation to a relative homotopy yields the original relative homotopy.

Русский

Повторное применение операции симметрии к относительной гомотопии возвращает исходную гомотопию.

LaTeX

$$$\forall F:\mathrm{HomotopyRel}(f_0,f_1;S),\ (F^{\mathrm{symm}})^{\mathrm{symm}} = F.$$$

Lean4

@[simp]
theorem symm_symm (F : HomotopyRel f₀ f₁ S) : F.symm.symm = F :=
  HomotopyWith.symm_symm F

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