symm — Mathlib

English

The relation Homotopic is an equivalence relation on generalized loops: reflexive, symmetric, and transitive.

Русский

Отношение гомотопии является эквалентностью на обобщённых петлях: рефлексивность, симметричность и транзитивность.

LaTeX

$$Equiv(Homotopic) with refl, symm, trans$$

Lean4

@[symm]
nonrec theorem symm (H : Homotopic f g) : Homotopic g f :=
  H.symm

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