mem_edgeSet

Mathlib.Combinatorics.SimpleGraph.Basic

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

English

An unordered pair {v,w} is an edge of G exactly when G.Adj(v,w).

Русский

Неупорядоченная пара {v,w} является ребром графа G тогда и только тогда, когда G.Adj(v,w).

LaTeX

$$$$ \{v,w\} \in E(G) \iff G.Adj(v,w). $$$$

Lean4

@[simp]
theorem mem_edgeSet : s(v, w) ∈ G.edgeSet ↔ G.Adj v w :=
  Iff.rfl

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

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

Разделы

Аффилиация

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