Simple graphs

This file defines two type classes for graphs Graph α β: Loopless and Simple.

Main definitions

• Loopless: a graph is loopless if it has no loops
• Simple: a graph is simple if it has no multiple edges between the same pair of vertices
• toSimpleGraph: a function that constructs a SimpleGraph V(G) from a Graph G
• ofSimpleGraph: a function that constructs a Graph α (Sym2 α) from a SimpleGraph α

TODO: Show ofSimpleGraph (toSimpleGraph G) is isomorphic to G when isomorphism on Graph is defined.

class Graph.Loopless {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

A loopless graph is one where the ends of every edge are distinct.

• not_isLoopAt (e : β) (x : α) : ¬G.IsLoopAt e x

theorem Graph.loopless_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Loopless ↔ ∀ (e : β) (x : α), ¬G.IsLoopAt e x

@[simp]

theorem Graph.not_isLoopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] (e : β) (x : α) : ¬G.IsLoopAt e x

theorem Graph.not_adj_self {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] (x : α) : ¬G.Adj x x

theorem Graph.Adj.ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} [G.Loopless] (hxy : G.Adj u v) : u ≠ v

theorem Graph.IsLink.ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} [G.Loopless] (he : G.IsLink e u v) : u ≠ v

theorem Graph.loopless_iff_forall_ne_of_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Loopless ↔ ∀ (u v : α), G.Adj u v → u ≠ v

theorem Graph.vertexSet_nontrivial_of_edgeSet_nonempty_of_loopless {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (hE : G.edgeSet.Nonempty) : G.vertexSet.Nontrivial

theorem Graph.Loopless.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} [hG : G.Loopless] (hle : H ≤ G) : H.Loopless

@[simp]

theorem Graph.Inc.isNonloopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {e : β} [G.Loopless] (h : G.Inc e u) : G.IsNonloopAt e u

class Graph.Simple {α : Type u_1} {β : Type u_2} (G : Graph α β) extends G.Loopless : Prop

A Simple graph is a Loopless graph where no pair of vertices are the ends of more than one edge.

• not_isLoopAt (e : β) (x : α) : ¬G.IsLoopAt e x
• eq_of_isLink ⦃e f : β⦄ ⦃x y : α⦄ : G.IsLink e x y → G.IsLink f x y → e = f

theorem Graph.simple_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.Simple ↔ G.Loopless ∧ ∀ ⦃e f : β⦄ ⦃x y : α⦄, G.IsLink e x y → G.IsLink f x y → e = f

theorem Graph.IsLink.eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e f : β} [G.Simple] (h : G.IsLink e u v) (h' : G.IsLink f u v) : e = f

theorem Graph.Simple.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.Simple] (hle : H ≤ G) : H.Simple

instance Graph.instSimpleNoEdge {α : Type u_1} {β : Type u_2} (V : Set α) : (noEdge V β).Simple

instance Graph.instSimpleBot {α : Type u_1} {β : Type u_2} : ⊥.Simple

def Graph.toSimpleGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : SimpleGraph ↑G.vertexSet

Construct a simple graph from a graph.

Equations

• G.toSimpleGraph = { Adj := fun (u v : ↑G.vertexSet) => u ≠ v ∧ G.Adj ↑u ↑v, symm := ⋯, loopless := ⋯ }

@[simp]

theorem Graph.toSimpleGraph_adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : ↑G.vertexSet) : G.toSimpleGraph.Adj u v = (u ≠ v ∧ G.Adj ↑u ↑v)

theorem Graph.toSimpleGraph_adj_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (u v : ↑G.vertexSet) : G.toSimpleGraph.Adj u v ↔ G.Adj ↑u ↑v

theorem Graph.toSimpleGraph_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤s H) : G.toSimpleGraph ≤ ⋯ ▸ H.toSimpleGraph

def Graph.ofSimpleGraph {α : Type u_1} (G : SimpleGraph α) : Graph α (Sym2 α)

Construct a graph from a simple graph. It has every element of the vertex type as a vertex.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Graph.vertexSet_ofSimpleGraph {α : Type u_1} (G : SimpleGraph α) : (ofSimpleGraph G).vertexSet = Set.univ

@[simp]

theorem Graph.edgeSet_ofSimpleGraph {α : Type u_1} (G : SimpleGraph α) : (ofSimpleGraph G).edgeSet = G.edgeSet

@[simp]

theorem Graph.ofSimpleGraph_isLink {α : Type u_1} (G : SimpleGraph α) (e : Sym2 α) (x y : α) : (ofSimpleGraph G).IsLink e x y = (e = s(x, y) ∧ e ∈ G.edgeSet)

@[simp]

theorem Graph.ofSimpleGraph_adj_iff {α : Type u_1} {G : SimpleGraph α} (u v : α) : (ofSimpleGraph G).Adj u v ↔ G.Adj u v

def Graph.toSimpleGraphOfSimpleGraphIso {α : Type u_1} (G : SimpleGraph α) : (ofSimpleGraph G).toSimpleGraph ≃g G

The isomorphism between toSimpleGraph (ofSimpleGraph G) and G.

Equations

• Graph.toSimpleGraphOfSimpleGraphIso G = { toEquiv := Equiv.Set.univ α, map_rel_iff' := ⋯ }