mem_edgeSet

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.mem_edgeSet

English

An unordered pair s(v,w) belongs to G'.edgeSet if and only if v and w are adjacent in G'.

Русский

Неупорядоченная пара вершин s(v,w) принадлежит G'.edgeSet тогда, когда v и w смежны в G'.

LaTeX

$$$s(v,w) \\in G'.edgeSet \\iff G'.Adj(v,w)$$$

Lean4

@[simp]
protected theorem mem_edgeSet {G' : Subgraph G} {v w : V} : s(v, w) ∈ G'.edgeSet ↔ G'.Adj v w :=
  .rfl

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

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

Разделы

Аффилиация

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