edge_symm

Mathlib.Combinatorics.SimpleGraph.Dart

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

English

The edge of a symmetric dart is the same as the edge of the original.

Русский

Ребро симметричной стрелы равно ребру исходной стрелы.

LaTeX

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

Lean4

@[simp]
theorem edge_symm (d : G.Dart) : d.symm.edge = d.edge :=
  Sym2.mk_prod_swap_eq

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

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

Разделы

Аффилиация

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