symm_symm

Mathlib.Combinatorics.SimpleGraph.Dart

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Dart.symm_symm

English

Taking symmetry twice returns the original dart.

Русский

Дважды применяя симметрию, получаем исходную стрелу.

LaTeX

$$$ d.symm.symm = d $$$

Lean4

@[simp]
theorem symm_symm (d : G.Dart) : d.symm.symm = d :=
  Dart.ext _ _ <| Prod.swap_swap _

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

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

Разделы

Аффилиация

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