edgeSet — Mathlib

English

The edge set of G consists of unordered pairs {v,w} for which G.Adj(v,w).

Русский

Множество ребер графа G состоит из неупорядоченных пар {v,w}, для которых G.Adj(v,w).

LaTeX

$$$$ E(G) = \{ \{v,w\} \mid G.Adj(v,w) \}. $$$$

Lean4

/-- `G.edgeSet` is the edge set for `G`.
This is an abbreviation for `edgeSetEmbedding G` that permits dot notation. -/
abbrev edgeSet (G : SimpleGraph V) : Set (Sym2 V) :=
  edgeSetEmbedding V G

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