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

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

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

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

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

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

theorem Graph.eq_noEdge_or_vertexSet_nontrivial {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Loopless] : G = ⊥ ∨ (∃ (x : α), G = Graph.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

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.finite_of_vertexSet_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] (h : G.vertexSet.Finite) : G.Finite

@[simp]

theorem Graph.Simple.vertexSet_finite_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] : G.vertexSet.Finite ↔ G.Finite

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

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

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

instance Graph.instSimpleVertexDelete {α : Type u_1} {β : Type u_2} {X : Set α} {G : Graph α β} [G.Simple] : (G - 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 α) : (Graph.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.incAdjEquiv {α : Type u_1} {β : Type u_2} (G : Graph α β) [G.Simple] (x : α) : { e : β // G.Inc e x } ≃ { y : α // G.Adj x y }

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

Equations

• G.incAdjEquiv x = { toFun := fun (e : { e : β // G.Inc e x }) => ⟨Exists.choose ⋯, ⋯⟩, invFun := fun (y : { y : α // G.Adj x y }) => ⟨Exists.choose ⋯, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Graph.isLink_incAdjEquiv {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} [G.Simple] (e : { e : β // G.Inc e 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.Inc e 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 : { y : α // G.Adj x y }) : 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 : { y : α // G.Adj x y }) : G.Inc (↑((G.incAdjEquiv x).symm y)) x

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