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} {x y : α} {G : Graph α β} [G.Loopless] (hxy : G.Adj x y) : x ≠ y

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

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

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

theorem Graph.Loopless.mono {α : 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} {x : α} {e : β} {G : Graph α β} [G.Loopless] (h : G.Inc e x) : G.IsNonloopAt e x

@[simp]

theorem Graph.setOf_isLoopAt_empty {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Loopless] : {e : β | G.IsLoopAt e x} = ∅

theorem Graph.setOf_isNonloopAt_incEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (x : α) : {e : β | G.IsNonloopAt e x} = E(G, x)

@[simp]

theorem Graph.setLinkEdges_singleton_compl_eq_incEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] (x : α) : E(G, {x}, G.vertexSet \ {x}) = E(G, x)

@[simp]

theorem Graph.IsComplete.neighbors {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Loopless] (h : G.IsComplete) (hx : x ∈ G.vertexSet) : N(G, x) = G.vertexSet \ {x}

instance Graph.instLooplessInduce {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (X : Set α) : G[X].Loopless

instance Graph.instLooplessDeleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (X : Set α) : (G.deleteVerts X).Loopless

instance Graph.instLooplessRestrict {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (F : Set β) : (G.restrict F).Loopless

instance Graph.instLooplessDeleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (F : Set β) : (G.deleteEdges F).Loopless

theorem Graph.eq_noEdge_or_vertexSet_nontrivial {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] : G = ⊥ ∨ (∃ (x : α), G = noEdge {x} β) ∨ G.vertexSet.Nontrivial

instance Graph.Loopless.union {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.Loopless] [H.Loopless] : (G ∪ H).Loopless

def Graph.loopRemove {α : Type u_1} {β : Type u_2} (G : Graph α β) : Graph α β

Maximally loopless subgraph of G.

Equations

• G.loopRemove = G.restrict {e : β | ∀ (x : α), ¬G.IsLoopAt e x}

@[simp]

theorem Graph.vertexSet_loopRemove {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.loopRemove.vertexSet = G.vertexSet

instance Graph.instLooplessLoopRemove {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.loopRemove.Loopless

theorem Graph.loopRemove_le {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.loopRemove ≤ G

theorem Graph.loopRemove_isSpanningSubgraph {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.loopRemove ≤s G

theorem Graph.loopRemove_deleteEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.loopRemove = G.deleteEdges (⋃ x ∈ G.vertexSet, loopSet x)

@[simp]

theorem Graph.loopRemove_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.loopRemove.edgeSet = {e : β | e ∈ G.edgeSet ∧ ∀ (x : α), ¬G.IsLoopAt e x}

theorem Graph.loopRemove_edgeSet_diff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.loopRemove.edgeSet = G.edgeSet \ ⋃ x ∈ G.vertexSet, loopSet x

@[simp]

theorem Graph.loopRemove_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : G.loopRemove.IsLink e x y ↔ G.IsLink e x y ∧ x ≠ y

theorem Graph.le_loopRemove {α : Type u_1} {β : Type u_2} {G H : Graph α β} [H.Loopless] (h : H ≤ G) : H ≤ G.loopRemove

Proof that loopRemove is the maximally loopless subgraph of G.

@[simp]

theorem Graph.loopRemove_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] : G.loopRemove = G

@[simp]

theorem Graph.loopRemove_eq_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] : G.loopRemove = G ↔ G.Loopless

theorem Graph.IsPath.loopRemove {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : G.loopRemove.IsPath P

theorem Graph.loopRemove_isSpanningSubgraph_deleteEdges_isLoopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : G.loopRemove ≤s G.deleteEdges {e : β | G.IsLoopAt e x}

theorem Graph.loopRemove_le_deleteEdges_isLoopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : G.loopRemove ≤ G.deleteEdges {e : β | G.IsLoopAt e x}

theorem Graph.IsLoopAt.loopRemove_isSpanningSubgraph_deleteEdges {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : G.loopRemove ≤s G.deleteEdges {e}

theorem Graph.IsLoopAt.loopRemove_le_deleteEdges {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : G.loopRemove ≤ G.deleteEdges {e}

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.unique_edge {α : Type u_1} {β : Type u_2} {x y : α} {e f : β} {G : Graph α β} [G.Simple] (h : G.IsLink e x y) (h' : G.IsLink f x y) : e = f

theorem Graph.ends_injective {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Simple] : Function.Injective G.ends

theorem Graph.Simple.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Simple) (hle : H ≤ G) : H.Simple

instance Graph.instSimpleRestrict {α : Type u_1} {β : Type u_2} {F : Set β} {G : Graph α β} [G.Simple] : (G.restrict F).Simple

instance Graph.instSimpleDeleteEdges {α : Type u_1} {β : Type u_2} {F : Set β} {G : Graph α β} [G.Simple] : (G.deleteEdges F).Simple

instance Graph.instSimpleDeleteVerts {α : Type u_1} {β : Type u_2} {X : Set α} {G : Graph α β} [G.Simple] : (G.deleteVerts X).Simple

instance Graph.instSimpleInduce {α : Type u_1} {β : Type u_2} {X : Set α} {G : Graph α β} [G.Simple] : G[X].Simple

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

theorem Graph.singleEdge_simple {α : Type u_1} {β : Type u_2} {x y : α} (hne : x ≠ y) (e : β) : (Graph.singleEdge x y e).Simple

noncomputable def Graph.adjIncFun {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : ↑N(G, x) → ↑E(G, x)

Equations

• G.adjIncFun x y = ⟨Exists.choose ⋯, ⋯⟩

theorem Graph.adjIncFun_injective {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : Function.Injective (G.adjIncFun x)

noncomputable def Graph.incAdjEquiv {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Simple] (x : α) : ↑E(G, x) ≃ ↑N(G, x)

In a simple graph, the bijection between edges at x and neighbours of x.

Equations

• G.incAdjEquiv x = { toFun := fun (e : ↑E(G, x)) => ⟨Exists.choose ⋯, ⋯⟩, invFun := fun (y : ↑N(G, x)) => G.adjIncFun x y, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Graph.isLink_incAdjEquiv {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (e : ↑E(G, x)) : G.IsLink (↑e) x ↑((G.incAdjEquiv x) e)

@[simp]

theorem Graph.adj_incAdjEquiv {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (e : ↑E(G, x)) : G.Adj x ↑((G.incAdjEquiv x) e)

@[simp]

theorem Graph.isLink_incAdjEquiv_symm {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (y : ↑N(G, x)) : G.IsLink (↑((G.incAdjEquiv x).symm y)) x ↑y

@[simp]

theorem Graph.inc_incAdjEquiv_symm {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (y : ↑N(G, x)) : G.Inc (↑((G.incAdjEquiv x).symm y)) x

@[simp]

theorem Graph.encard_incEdges {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Simple] (x : α) : E(G, x).encard = N(G, x).encard

Operations

theorem Graph.Simple.union {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.Simple] [H.Simple] (h : ∀ ⦃e f : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink f x y → e = f) : (G ∪ H).Simple

theorem Graph.IsPath.toGraph_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) : P.toGraph.Simple

Small Graphs

theorem Graph.eq_banana {α : Type u_1} {β : Type u_2} {a b : α} {G : Graph α β} [G.Loopless] (hV : G.vertexSet = {a, b}) : G = banana a b G.edgeSet

theorem Graph.exists_eq_banana {α : Type u_1} {β : Type u_2} {a b : α} {G : Graph α β} [G.Loopless] (hV : G.vertexSet = {a, b}) : ∃ (F : Set β), G = banana a b F

theorem Graph.exists_eq_banana_of_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Loopless] (hV : G.vertexSet.encard = 2) : ∃ (a : α) (b : α) (F : Set β), a ≠ b ∧ G = banana a b F

theorem Graph.banana_loopless {α : Type u_1} {a b : α} (hab : a ≠ b) (F : Set α) : (banana a b F).Loopless

instance Graph.lineGraph_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.LineGraph.Simple

instance Graph.mixedLineGraph_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.mixedLineGraph.Simple

instance Graph.completeGraph_simple {n : ℕ} : (CompleteGraph n).Simple

instance Graph.completeBipartiteGraph_simple {m n : ℕ} : (CompleteBipartiteGraph m n).Simple

@[simp]

theorem Graph.encard_setLinkEdges_singleton_compl_completeGraph (n x : ℕ) (hx : x < n) : E(CompleteGraph n, {x}, (CompleteGraph n).vertexSet \ {x}).encard = ↑(n - 1)

def Graph.simplify {α : Type u_1} {β : Type u_2} (G : Graph α β) (φ : β → β) : Graph α β

Equations

• G.simplify φ = G.loopRemove.restrict (φ '' G.edgeSet)

@[simp]

theorem Graph.vertexSet_simplify {α : Type u_1} {β : Type u_2} (G : Graph α β) (φ : β → β) : (G.simplify φ).vertexSet = G.vertexSet

theorem Graph.simplify_isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} : G.simplify φ ≤s G

theorem Graph.simplify_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} : G.simplify φ ≤ G

theorem Graph.simplify_edgeSet_diff {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} (hφ : G.parallelClasses.IsRepFun φ) : (G.simplify φ).edgeSet = φ '' G.edgeSet \ ⋃ x ∈ G.vertexSet, loopSet x

theorem Graph.simplify_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} (hφ : G.parallelClasses.IsRepFun φ) : (G.simplify φ).edgeSet = φ '' (G.edgeSet \ ⋃ x ∈ G.vertexSet, loopSet x)

theorem Graph.simplify_eq_restrict {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} (hφ : G.parallelClasses.IsRepFun φ) : G.simplify φ = G.restrict (φ '' (G.edgeSet \ ⋃ x ∈ G.vertexSet, loopSet x))