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]

instance Graph.noEdge_loopless {α : Type u_1} {X : Set α} {β : Type u_3} : (noEdge X β).Loopless

@[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

theorem Graph.Compatible.loopless_union_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G.Compatible H) : (G ∪ H).Loopless ↔ G.Loopless ∧ 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

@[simp]

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

@[simp]

theorem Graph.singleEdge_loopless_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : (Graph.singleEdge x y e).Loopless ↔ x ≠ y

@[simp]

instance Graph.noEdge_simple {α : Type u_1} {X : Set α} {β : Type u_3} : (noEdge X β).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.Compatible.simple_union_iff {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G.Compatible H) : (G ∪ H).Simple ↔ G.Simple ∧ H.Simple ∧ ∀ ⦃e f : β⦄ ⦃x y : α⦄, G.IsLink e x y → H.IsLink f x y → e = f

theorem Graph.Compatible.simple_union_iff_of_subsingleton_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G.Compatible H) (hss : (G.vertexSet ∩ H.vertexSet).Subsingleton) : (G ∪ H).Simple ↔ G.Simple ∧ H.Simple

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

theorem Graph.IsCyclicWalk.toGraph_loopless_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.toGraph.Loopless ↔ C.length ≠ 1

theorem Graph.IsCyclicWalk.toGraph_simple_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.toGraph.Simple ↔ 3 ≤ C.length

theorem Graph.IsCyclicWalk.three_le_length_of_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} [G.Simple] (hC : G.IsCyclicWalk P) : 3 ≤ P.length

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.IsSimpleficationOf {α : Type u_1} {β : Type u_2} (G H : Graph α β) : Prop

G is a simplefication of H if G is maximally simple subgraph of H.

Equations

• G.IsSimpleficationOf H = Maximal (fun (G : Graph α β) => G.Simple ∧ G ≤ H) G

theorem Graph.IsSimpleficationOf.simple {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.IsSimpleficationOf H) : G.Simple

theorem Graph.IsSimpleficationOf.le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.IsSimpleficationOf H) : G ≤ H

theorem Graph.IsSimpleficationOf.isSpanningSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.IsSimpleficationOf H) : G ≤s H

theorem Graph.IsSimpleficationOf.adj_iff {α : Type u_1} {β : Type u_2} {x y : α} {G H : Graph α β} (h : G.IsSimpleficationOf H) (hne : x ≠ y) : G.Adj x y ↔ H.Adj x y

theorem Graph.IsSimpleficationOf.induce {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.IsSimpleficationOf H) (X : Set α) : G[X].IsSimpleficationOf H[X]

theorem Graph.IsSimpleficationOf.deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.IsSimpleficationOf H) (X : Set α) : (G.deleteVerts X).IsSimpleficationOf (H.deleteVerts X)

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_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {φ : β → β} : (G.simplify φ).IsLink e x y ↔ e ∈ φ '' G.edgeSet ∧ G.IsLink e x y ∧ x ≠ y

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))

theorem Graph.simplify_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} (hφ : G.parallelClasses.IsRepFun φ) : (G.simplify φ).Simple

theorem Graph.simplify_isSimpleficationOf {α : Type u_1} {β : Type u_2} {G : Graph α β} {φ : β → β} (hφ : G.parallelClasses.IsRepFun φ) : (G.simplify φ).IsSimpleficationOf G

theorem Graph.exists_isSimpleficationOf_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G ≤ H) [G.Simple] : ∃ (G' : Graph α β), G ≤ G' ∧ G'.IsSimpleficationOf H

theorem Graph.IsCyclicWalk.nontrivial_of_loopless {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} [G.Loopless] (hC : G.IsCyclicWalk P) : P.Nontrivial

theorem Graph.map_loopless_iff {α : Type u_1} {β : Type u_2} {α' : Type u_3} {φ : α → α'} {G : Graph α β} : (map φ G).Loopless ↔ ∀ (x y : α), G.Adj x y → φ x ≠ φ y

theorem Graph.Loopless.map {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} (hG : G.Loopless) {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (Graph.map φ G).Loopless

theorem Graph.map_loopless_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).Loopless ↔ G.Loopless

@[simp]

theorem Graph.edgeMap_loopless_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_4} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).Loopless ↔ G.Loopless

theorem Graph.map_simple_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} : (map φ G).Simple ↔ (∀ (x y : α), G.Adj x y → φ x ≠ φ y) ∧ ∀ (e : β) (x y : α) (e' : β) (x' y' : α), G.IsLink e x y → G.IsLink e' x' y' → φ x = φ x' → φ y = φ y' → e = e'

theorem Graph.map_simple_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {α' : Type u_3} {φ : α → α'} (hφ : Set.InjOn φ G.vertexSet) : (map φ G).Simple ↔ G.Simple

theorem Graph.edgeMap_simple_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_4} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} : (G.edgeMap φ hφ).Simple ↔ G.Loopless ∧ ∀ (x y : α) (e f : β), G.IsLink e x y → G.IsLink f x y → φ e = φ f

theorem Graph.edgeMap_simple_iff_of_injOn {α : Type u_1} {β : Type u_2} {G : Graph α β} {β' : Type u_4} {φ : β → β'} {hφ : ∀ e₁ ∈ G.edgeSet, ∀ e₂ ∈ G.edgeSet, φ e₁ = φ e₂ → G.IsLink e₁ = G.IsLink e₂} (hφ' : Set.InjOn φ G.edgeSet) : (G.edgeMap φ hφ).Simple ↔ G.Simple