edge_comm

Mathlib.Combinatorics.SimpleGraph.Operations

URI: https://scilib.ai/kg/mathlib#SimpleGraph.edge_comm

English

The edge relation is symmetric: edge s t = edge t s.

Русский

Связь ребра симметрична: edge(s,t) = edge(t,s).

LaTeX

$$$ \text{edge}(s,t) = \text{edge}(t,s) $$$

Lean4

theorem edge_comm : edge s t = edge t s := by rw [edge, edge, Sym2.eq_swap]

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

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

Разделы

Аффилиация

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