fromEdgeSet — Mathlib

English

From a set s of edges, define a simple graph with adjacency if and only if the unordered pair is in s and the vertices are distinct.

Русский

Из множества рёбер s задаём простой граф: две вершины смежны тогда, когда неупорядоченная пара вершин принадлежит s и вершины различны.

LaTeX

$$$\\text{Adj}_{\\mathrm{fromEdgeSet}(s)}(v,w) \\;\\Leftrightarrow\\; (\\{v,w\\} \\in s) \\wedge v \\neq w$$$

Lean4

/-- `fromEdgeSet` constructs a `SimpleGraph` from a set of edges, without loops. -/
def fromEdgeSet : SimpleGraph V where
  Adj := Sym2.ToRel s ⊓ Ne
  symm _ _ h := ⟨Sym2.toRel_symmetric s h.1, h.2.symm⟩

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