edge_comp_symm

Mathlib.Combinatorics.SimpleGraph.Dart

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

English

The edge is preserved under taking symmetry: edge of the symmetric of d equals edge of d.

Русский

Ребро сохраняется при применения симметрии: edge(д^{symm}) = edge(d).

LaTeX

$$$ \operatorname{edge}(\operatorname{symm}(d)) = \operatorname{edge}(d) $$$

Lean4

@[simp]
theorem edge_comp_symm : Dart.edge ∘ Dart.symm = (Dart.edge : G.Dart → Sym2 V) :=
  funext Dart.edge_symm

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

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

Разделы

Аффилиация

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