Theorems · Inductive type · combinatorics

Graph

Type u_3 → Type u_4 → Type (max u_3 u_4)

A multigraph with vertices of type α and edges of type β, as described by vertex and edge sets vertexSet : Set α and edgeSet : Set β, and a predicate IsLink describing whether an edge e : β has vertices x y : α as its ends. The edgeSet structure field can be inferred from IsLink via edge_mem_iff_exists_isLink (and this structure provides default values for edgeSet and edge_mem_iff_exists_isLink that use IsLink). While the field is not strictly necessary, when defining a graph we often immediately know what the edge set should be, and furthermore having edgeSet separate can be convenient for definitional equality reasons.

Defined in

Mathlib.Combinatorics.Graph.Basic

Cited by

242 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms