Multigraphs

A multigraph is a set of vertices and a set of edges, together with incidence data that associates each edge e with an unordered pair s(x,y) of vertices called the ends of e. The pair of e and s(x,y) is called a link. The vertices x and y may be equal, in which case e is a loop. There may be more than one edge with the same ends.

If a multigraph has no loops and has at most one edge for every given ends, it is called simple, and these objects are also formalized as SimpleGraph.

This module defines Graph α β for a vertex type α and an edge type β, and gives basic API for incidence, adjacency and extensionality. The design broadly follows [Chou1994].

Main definitions

For G : Graph α β, ...

• V(G) denotes the vertex set of G as a term in Set α.
• E(G) denotes the edge set of G as a term in Set β.
• G.IsLink e x y means that the edge e : β has vertices x : α and y : α as its ends.
• G.Inc e x means that the edge e : β has x as one of its ends.
• G.Adj x y means that there is an edge e having x and y as its ends.
• G.IsLoopAt e x means that e is a loop edge with both ends equal to x.
• G.IsNonloopAt e x means that e is a non-loop edge with one end equal to x.
• G.incidenceSet x is the set of edges incident to x.
• G.loopSet x is the set of loops with both ends equal to x.
• G.copy creates a definitional copy of a graph with propositionally equal data.
• G.Compatible H means that G and H agree on the incidence relation for their shared edges.
• Graph.noEdge V is the graph with vertex set V and no edges.
• Graph.bouquet v E is the graph with vertex set {v} and edge set E, where every edge is a loop at v.
• Graph.banana u v E is the graph with vertex set {u, v} and edge set E, where every edge connects u and v.

Implementation notes

Unlike the design of SimpleGraph, the vertex and edge sets of G are modelled as sets V(G) : Set α and E(G) : Set β, within ambient types, rather than being types themselves. This mimics the 'embedded set' design used in Matroid, which seems to be more convenient for formalizing real-world proofs in combinatorics.

A specific advantage is that this allows subgraphs of G : Graph α β to also exist on an equal footing with G as terms in Graph α β, and so there is no need for a Graph.subgraph type and all the associated definitions and canonical coercion maps. The same will go for minors and the various other partial orders on multigraphs.

The main tradeoff is that parts of the API will need to care about whether a term x : α or e : β is a 'real' vertex or edge of the graph, rather than something outside the vertex or edge set. This is an issue, but is likely amenable to automation.

Notation

Reflecting written mathematics, we use the compact notations V(G) and E(G) to refer to the vertexSet and edgeSet of G : Graph α β. If G.IsLink e x y then we refer to e as edge and x and y as left and right in names.

structure 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.

• vertexSet : Set α

  The vertex set.

• IsLink : β → α → α → Prop

  The binary incidence predicate, stating that x and y are the ends of an edge e. If G.IsLink e x y then we refer to e as edge and x and y as left and right.

• edgeSet : Set β

  The edge set.

• isLink_symm ⦃e : β⦄ : e ∈ self.edgeSet → Symmetric (self.IsLink e)

  If e goes from x to y, it goes from y to x.

• eq_or_eq_of_isLink_of_isLink ⦃e : β⦄ ⦃x y v w : α⦄ : self.IsLink e x y → self.IsLink e v w → x = v ∨ x = w

  An edge is incident with at most one pair of vertices.

• edge_mem_iff_exists_isLink (e : β) : e ∈ self.edgeSet ↔ ∃ (x : α) (y : α), self.IsLink e x y

  An edge e is incident to something if and only if e is in the edge set.

• left_mem_of_isLink ⦃e : β⦄ ⦃x y : α⦄ : self.IsLink e x y → x ∈ self.vertexSet

  If some edge e is incident to x, then x ∈ V.

def Graph.«termV(_)» : Lean.ParserDescr

V(G) denotes the vertexSet of a graph G.

def Graph.«termE(_)» : Lean.ParserDescr

E(G) denotes the edgeSet of a graph G.

Edge-vertex-vertex incidence

theorem Graph.IsLink.edge_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : e ∈ G.edgeSet

@[simp]

theorem Graph.not_isLink_of_notMem_edgeSet {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) : ¬G.IsLink e x y

theorem Graph.IsLink.symm {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.IsLink e y x

theorem Graph.IsLink.left_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : x ∈ G.vertexSet

theorem Graph.IsLink.right_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : y ∈ G.vertexSet

theorem Graph.isLink_comm {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : G.IsLink e x y ↔ G.IsLink e y x

theorem Graph.exists_isLink_of_mem_edgeSet {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (h : e ∈ G.edgeSet) : ∃ (x : α) (y : α), G.IsLink e x y

theorem Graph.edgeSet_eq_setOf_exists_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.edgeSet = {e : β | ∃ (x : α) (y : α), G.IsLink e x y}

theorem Graph.IsLink.left_eq_or_eq {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e z w) : x = z ∨ x = w

theorem Graph.IsLink.right_eq_or_eq {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e z w) : y = z ∨ y = w

theorem Graph.IsLink.left_eq_of_right_ne {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e z w) (hzx : x ≠ z) : x = w

theorem Graph.IsLink.right_unique {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e x z) : y = z

theorem Graph.IsLink.left_unique {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x z) (h' : G.IsLink e y z) : x = y

theorem Graph.IsLink.eq_and_eq_or_eq_and_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {x' y' : α} (h : G.IsLink e x y) (h' : G.IsLink e x' y') : x = x' ∧ y = y' ∨ x = y' ∧ y = x'

theorem Graph.IsLink.isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) {x' y' : α} : G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

theorem Graph.IsLink.isLink_iff_sym2_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) {x' y' : α} : G.IsLink e x' y' ↔ s(x, y) = s(x', y')

Edge-vertex incidence

def Graph.Inc {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

The unary incidence predicate of G. G.Inc e x means that the vertex x is one or both of the ends of the edge e. In the Inc namespace, we use edge and vertex to refer to e and x.

theorem Graph.Inc.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : e ∈ G.edgeSet

@[simp]

theorem Graph.not_inc_of_notMem_edgeSet {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (he : e ∉ G.edgeSet) : ¬G.Inc e x

theorem Graph.Inc.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : x ∈ G.vertexSet

theorem Graph.IsLink.inc_left {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.Inc e x

theorem Graph.IsLink.inc_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.Inc e y

theorem Graph.Inc.eq_or_eq_of_isLink {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.Inc e x) (h' : G.IsLink e y z) : x = y ∨ x = z

theorem Graph.Inc.eq_of_isLink_of_ne_left {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.Inc e x) (h' : G.IsLink e y z) (hxy : x ≠ y) : x = z

theorem Graph.IsLink.isLink_iff_eq {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.IsLink e x z ↔ z = y

theorem Graph.isLink_iff_inc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y

The binary incidence predicate can be expressed in terms of the unary one.

noncomputable def Graph.Inc.other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : α

Given a proof that the edge e is incident with the vertex x in G, noncomputably find the other end of e. (If e is a loop, this is equal to x itself).

@[simp]

theorem Graph.Inc.isLink_other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : G.IsLink e x h.other

@[simp]

theorem Graph.Inc.inc_other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : G.Inc e h.other

theorem Graph.Inc.eq_or_eq_or_eq {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (hx : G.Inc e x) (hy : G.Inc e y) (hz : G.Inc e z) : x = y ∨ x = z ∨ y = z

theorem Graph.inc_eq_inc_iff_isLink_eq_isLink {α : Type u_1} {β : Type u_2} {e f : β} {G₁ G₂ : Graph α β} : G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f

def Graph.IsLoopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

G.IsLoopAt e x means that both ends of the edge e are equal to the vertex x.

@[simp]

theorem Graph.isLink_self_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsLink e x x ↔ G.IsLoopAt e x

theorem Graph.IsLoopAt.inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : G.Inc e x

theorem Graph.IsLoopAt.eq_of_inc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) (h' : G.Inc e y) : x = y

theorem Graph.IsLoopAt.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : e ∈ G.edgeSet

theorem Graph.IsLoopAt.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : x ∈ G.vertexSet

def Graph.IsNonloopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

G.IsNonloopAt e x means that the vertex x is one but not both of the ends of the edge =e, or equivalently that e is incident with x but not a loop at x - see Graph.isNonloopAt_iff_inc_not_isLoopAt.

theorem Graph.IsNonloopAt.inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : G.Inc e x

theorem Graph.IsNonloopAt.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : e ∈ G.edgeSet

theorem Graph.IsNonloopAt.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : x ∈ G.vertexSet

theorem Graph.IsLoopAt.not_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) (y : α) : ¬G.IsNonloopAt e y

theorem Graph.IsNonloopAt.not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) (y : α) : ¬G.IsLoopAt e y

theorem Graph.isNonloopAt_iff_inc_not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsNonloopAt e x ↔ G.Inc e x ∧ ¬G.IsLoopAt e x

theorem Graph.isLoopAt_iff_inc_not_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsLoopAt e x ↔ G.Inc e x ∧ ¬G.IsNonloopAt e x

theorem Graph.Inc.isLoopAt_or_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : G.IsLoopAt e x ∨ G.IsNonloopAt e x

Adjacency

def Graph.Adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : Prop

G.Adj x y means that G has an edge whose ends are the vertices x and y.

theorem Graph.Adj.symm {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : G.Adj y x

instance Graph.instSymmAdj {α : Type u_1} {β : Type u_2} {G : Graph α β} : Std.Symm G.Adj

theorem Graph.adj_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} (x y : α) : G.Adj x y ↔ G.Adj y x

theorem Graph.Adj.left_mem {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : x ∈ G.vertexSet

theorem Graph.Adj.right_mem {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : y ∈ G.vertexSet

theorem Graph.IsLink.adj {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.Adj x y

Extensionality

@[simp]

theorem Graph.mk_eq_self {α : Type u_1} {β : Type u_2} (G : Graph α β) {E : Set β} (hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y) : { vertexSet := G.vertexSet, IsLink := G.IsLink, edgeSet := E, isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ } = G

edgeSet can be determined using IsLink, so the graph constructed from G.vertexSet and G.IsLink using any value for edgeSet is equal to G itself.

theorem Graph.ext {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β} (hV : G₁.vertexSet = G₂.vertexSet) (h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y) : G₁ = G₂

Two graphs with the same vertex set and binary incidences are equal. (We use this as the default extensionality lemma rather than adding @[ext] to the definition of Graph, so it doesn't require equality of the edge sets.)

theorem Graph.ext_iff {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β} : G₁ = G₂ ↔ G₁.vertexSet = G₂.vertexSet ∧ ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y

theorem Graph.ext_inc {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β} (hV : G₁.vertexSet = G₂.vertexSet) (h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x) : G₁ = G₂

Two graphs with the same vertex set and unary incidences are equal.

def Graph.copy {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop} (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet) (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) : Graph α β

Graph.copy produces a graph equal to G but with provided definitional choices for vertexSet, edgeSet, and IsLink. This is mainly useful for improving definitional equalities while keeping the same underlying graph.

@[simp]

theorem Graph.copy_edgeSet {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop} (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet) (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) : (G.copy hvertexSet hedgeSet hIsLink).edgeSet = edgeSet

@[simp]

theorem Graph.copy_vertexSet {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop} (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet) (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) : (G.copy hvertexSet hedgeSet hIsLink).vertexSet = vertexSet

@[simp]

theorem Graph.copy_isLink {α : Type u_1} {β : Type u_2} (G : Graph α β) {vertexSet : Set α} {edgeSet : Set β} {IsLink : β → α → α → Prop} (hvertexSet : G.vertexSet = vertexSet) (hedgeSet : G.edgeSet = edgeSet) (hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) (a✝ : β) (a✝¹ a✝² : α) : (G.copy hvertexSet hedgeSet hIsLink).IsLink a✝ a✝¹ a✝² = IsLink a✝ a✝¹ a✝²

@[simp]

theorem Graph.copy_eq {α : Type u_1} {β : Type u_2} (G : Graph α β) {V : Set α} {E : Set β} {IsLink : β → α → α → Prop} (hV : G.vertexSet = V) (hE : G.edgeSet = E) (h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y) : G.copy hV hE h_isLink = G

Sets of edges or loops incident to a vertex

def Graph.incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : Set β

G.incidenceSet x is the set of edges incident to x in G.

@[simp]

theorem Graph.mem_incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) (e : β) : e ∈ incidenceSet x ↔ G.Inc e x

theorem Graph.incidenceSet_subset_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : incidenceSet x ⊆ G.edgeSet

def Graph.loopSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : Set β

G.loopSet x is the set of loops at x in G.

@[simp]

theorem Graph.mem_loopSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) (e : β) : e ∈ loopSet x ↔ G.IsLoopAt e x

theorem Graph.loopSet_subset_incidenceSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (x : α) : loopSet x ⊆ incidenceSet x

The loopSet is included in the incidenceSet.

Compatibility of Graphs

We define two graphs to be Compatible if for each edge belonging to their shared edge set, the incidence relation (i.e., which pairs of vertices it links) is the same in both graphs.

def Graph.Compatible {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Prop

Two graphs are compatible if their shared edges have the same ends in both graphs.

theorem Graph.Compatible.isLink_congr {α : Type u_1} {β : Type u_2} {e : β} {G H : Graph α β} (heG : e ∈ G.edgeSet) (heH : e ∈ H.edgeSet) (h : G.Compatible H) {x y : α} : G.IsLink e x y ↔ H.IsLink e x y

theorem Graph.Compatible.refl {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Compatible G

@[simp]

theorem Graph.Compatible.rfl {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Compatible G

instance Graph.instReflCompatible {α : Type u_1} {β : Type u_2} : Std.Refl Compatible

theorem Graph.Compatible.symm {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) : H.Compatible G

instance Graph.instSymmCompatible {α : Type u_1} {β : Type u_2} : Std.Symm Compatible

theorem Graph.IsLink.of_compatible {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) (h : G.IsLink e x y) : H.IsLink e x y

theorem Graph.Compatible.of_disjoint_edgeSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : Disjoint G.edgeSet H.edgeSet) : G.Compatible H

theorem Graph.Inc.of_compatible {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) (h : G.Inc e x) : H.Inc e x

theorem Graph.IsLoopAt.of_compatible {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) (h : G.IsLoopAt e x) : H.IsLoopAt e x

theorem Graph.IsNonloopAt.of_compatible {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β} (hGH : G.Compatible H) (heH : e ∈ H.edgeSet) (h : G.IsNonloopAt e x) : H.IsNonloopAt e x

Graphs with no edges

def Graph.noEdge {α : Type u_1} (vertexSet : Set α) (β : Type u_3) : Graph α β

The graph with vertex set vertexSet and no edges

@[simp]

theorem Graph.noEdge_edgeSet {α : Type u_1} (vertexSet : Set α) (β : Type u_3) : (noEdge vertexSet β).edgeSet = ∅

@[simp]

theorem Graph.noEdge_vertexSet {α : Type u_1} (vertexSet : Set α) (β : Type u_3) : (noEdge vertexSet β).vertexSet = vertexSet

@[simp]

theorem Graph.noEdge_isLink {α : Type u_1} (vertexSet : Set α) (β : Type u_3) (x✝ : β) (x✝¹ x✝² : α) : (noEdge vertexSet β).IsLink x✝ x✝¹ x✝² = False

theorem Graph.edgeSet_eq_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.edgeSet = ∅ ↔ G = noEdge G.vertexSet β

Graphs with two vertices

def Graph.banana {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β) : Graph α β

A graph with exactly two vertices and no loops.

@[simp]

theorem Graph.banana_isLink {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β) (e : β) (x y : α) : (banana u v edgeSet).IsLink e x y = (e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u))

@[simp]

theorem Graph.banana_edgeSet {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β) : (banana u v edgeSet).edgeSet = edgeSet

@[simp]

theorem Graph.banana_vertexSet {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β) : (banana u v edgeSet).vertexSet = {u, v}

@[simp]

theorem Graph.banana_inc {α : Type u_1} {β : Type u_2} {x u v : α} {e : β} {edgeSet : Set β} : (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)

theorem Graph.banana_comm {α : Type u_1} {β : Type u_2} (u v : α) (edgeSet : Set β) : banana u v edgeSet = banana v u edgeSet

@[simp]

theorem Graph.banana_isNonloopAt {α : Type u_1} {β : Type u_2} {x u v : α} {e : β} {edgeSet : Set β} : (banana u v edgeSet).IsNonloopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v

@[simp]

theorem Graph.banana_isLoopAt {α : Type u_1} {β : Type u_2} {x u v : α} {e : β} {edgeSet : Set β} : (banana u v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = u ∧ u = v

@[simp]

theorem Graph.banana_adj {α : Type u_1} {β : Type u_2} {x y u v : α} {edgeSet : Set β} : (banana u v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ s(x, y) = s(u, v)

@[simp]

theorem Graph.banana_empty {α : Type u_1} {β : Type u_2} {u v : α} : banana u v ∅ = noEdge {u, v} β

Graphs with one vertex

@[reducible, inline]

abbrev Graph.bouquet {α : Type u_1} {β : Type u_2} (v : α) (edgeSet : Set β) : Graph α β

A graph with one vertex and loops at that vertex. This is an abbreviation for the special case of banana where the two vertices are the same. Most lemmas about bouquet should instead be proved using banana instead.

theorem Graph.bouquet_vertexSet {α : Type u_1} {β : Type u_2} (v : α) (edgeSet : Set β) : (bouquet v edgeSet).vertexSet = {v}

theorem Graph.bouquet_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} (v : α) (edgeSet : Set β) : (bouquet v edgeSet).IsLink e x y ↔ e ∈ edgeSet ∧ x = v ∧ y = v

theorem Graph.bouquet_inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} (v : α) (edgeSet : Set β) : (bouquet v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ x = v

theorem Graph.bouquet_adj {α : Type u_1} {β : Type u_2} {x y : α} (v : α) (edgeSet : Set β) : (bouquet v edgeSet).Adj x y ↔ edgeSet.Nonempty ∧ x = v ∧ y = v

theorem Graph.bouquet_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} (v : α) (edgeSet : Set β) : (bouquet v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = v

theorem Graph.not_isNonloopAt_bouquet {α : Type u_1} {β : Type u_2} {x v : α} {e : β} {edgeSet : Set β} : ¬(bouquet v edgeSet).IsNonloopAt e x

theorem Graph.eq_bouquet_of_subsingleton {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} (hv : v ∈ G.vertexSet) (hss : G.vertexSet.Subsingleton) : G = bouquet v G.edgeSet

Every graph on just one vertex is a bouquet on that vertex.

theorem Graph.eq_bouquet_iff {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} : G = bouquet v G.edgeSet ↔ G.vertexSet = {v}

theorem Graph.exists_eq_bouquet {α : Type u_1} {β : Type u_2} {G : Graph α β} (hne : G.vertexSet.Nonempty) (hss : G.vertexSet.Subsingleton) : ∃ (x : α) (F : Set β), G = bouquet x F

Every graph on just one vertex is a bouquet on that vertex.

theorem Graph.bouquet_empty {α : Type u_1} {β : Type u_2} (v : α) : bouquet v ∅ = noEdge {v} β