symm

Mathlib.Combinatorics.Graph.Basic

URI: https://scilib.ai/kg/mathlib#Graph.IsLink.symm

English

IsLink is symmetric in the endpoints: if e links x to y, it links y to x.

Русский

IsLink симметричен по концам: если e соединяет x и y, он соединяет y и x.

LaTeX

$$$\\text{IsLink}(G,e,x,y) \\Rightarrow \\text{IsLink}(G,e,y,x).$$$

Lean4

protected theorem symm (h : G.IsLink e x y) : G.IsLink e y x :=
  G.isLink_symm h.edge_mem h

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

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

Разделы

Аффилиация

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