Constructions

@[simp]

theorem Graph.noEdge_eDegree {α : Type u_1} (V : Set α) (β : Type u_3) (x : α) : (noEdge V β).eDegree x = 0

@[simp]

theorem Graph.noEdge_degree {α : Type u_1} (V : Set α) (β : Type u_3) (x : α) : (noEdge V β).degree x = 0

theorem Graph.singleEdge_eDegree_left {α : Type u_1} {β : Type u_2} {x y : α} (hxy : x ≠ y) (e : β) : (Graph.singleEdge x y e).eDegree x = 1

theorem Graph.singleEdge_eDegree_right {α : Type u_1} {β : Type u_2} {x y : α} (hxy : x ≠ y) (e : β) : (Graph.singleEdge x y e).eDegree y = 1

theorem Graph.singleEdge_eDegree_of_ne {α : Type u_1} {β : Type u_2} {x y z : α} (e : β) (hx : z ≠ x) (hy : z ≠ y) : (Graph.singleEdge x y e).eDegree z = 0

theorem Graph.singleEdge_degree_left {α : Type u_1} {β : Type u_2} {x y : α} (hxy : x ≠ y) (e : β) : (Graph.singleEdge x y e).degree x = 1

theorem Graph.singleEdge_degree_right {α : Type u_1} {β : Type u_2} {x y : α} (hxy : x ≠ y) (e : β) : (Graph.singleEdge x y e).degree y = 1

theorem Graph.singleEdge_degree_of_ne {α : Type u_1} {β : Type u_2} {x y z : α} (e : β) (hx : z ≠ x) (hy : z ≠ y) : (Graph.singleEdge x y e).degree z = 0

theorem Graph.singleEdge_regular {α : Type u_1} {β : Type u_2} {x y : α} (hxy : x ≠ y) (e : β) : (Graph.singleEdge x y e).Regular 1

@[simp]

theorem Graph.singleEdge_self_eDegree {α : Type u_1} {β : Type u_2} (x : α) (e : β) : (Graph.singleEdge x x e).eDegree x = 2

@[simp]

theorem Graph.singleEdge_self_degree {α : Type u_1} {β : Type u_2} (x : α) (e : β) : (Graph.singleEdge x x e).degree x = 2

theorem Graph.banana_eDegree_left {α : Type u_1} {a b : α} (hab : a ≠ b) (F : Set α) : (banana a b F).eDegree a = F.encard

theorem Graph.banana_eDegree_right {α : Type u_1} {a b : α} (hab : a ≠ b) (F : Set α) : (banana a b F).eDegree b = F.encard

theorem Graph.banana_degree_left {α : Type u_1} {a b : α} (hab : a ≠ b) (F : Set α) : (banana a b F).degree a = F.ncard

theorem Graph.banana_degree_right {α : Type u_1} {a b : α} (hab : a ≠ b) (F : Set α) : (banana a b F).degree b = F.ncard

theorem Graph.union_incFun_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hdj : Disjoint G.edgeSet H.edgeSet) : (G ∪ H).incFun = G.incFun + H.incFun

theorem Graph.union_eDegree_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hdj : Disjoint G.edgeSet H.edgeSet) (x : α) : (G ∪ H).eDegree x = G.eDegree x + H.eDegree x

theorem Graph.eDegree_addEdge_left {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {a b : α} (he : e ∉ G.edgeSet) (hab : a ≠ b) : (G.addEdge e a b).eDegree a = G.eDegree a + 1

theorem Graph.eDegree_addEdge_right {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} {a b : α} (he : e ∉ G.edgeSet) (hab : a ≠ b) : (G.addEdge e a b).eDegree b = G.eDegree b + 1

theorem Graph.eDegree_addEdge_of_ne {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {a b : α} (he : e ∉ G.edgeSet) (hxa : x ≠ a) (hxb : x ≠ b) : (G.addEdge e a b).eDegree x = G.eDegree x

theorem Graph.union_degree_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.LocallyFinite] [H.LocallyFinite] (hdj : Disjoint G.edgeSet H.edgeSet) (x : α) : (G ∪ H).degree x = G.degree x + H.degree x

theorem Graph.degree_addEdge_left {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} [G.LocallyFinite] {a b : α} (he : e ∉ G.edgeSet) (hab : a ≠ b) : (G.addEdge e a b).degree a = G.degree a + 1

theorem Graph.degree_addEdge_right {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} [G.LocallyFinite] {a b : α} (he : e ∉ G.edgeSet) (hab : a ≠ b) : (G.addEdge e a b).degree b = G.degree b + 1

theorem Graph.degree_addEdge_of_ne {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} {a b : α} (he : e ∉ G.edgeSet) (hxa : x ≠ a) (hxb : x ≠ b) : (G.addEdge e a b).degree x = G.degree x

theorem Graph.IsNonloopAt.eDegree_delete_add_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (he : G.IsNonloopAt e x) : (G.deleteEdges {e}).eDegree x + 1 = G.eDegree x

theorem Graph.IsNonloopAt.degree_delete_add_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (he : G.IsNonloopAt e x) : (G.deleteEdges {e}).degree x + 1 = G.degree x

theorem Graph.IsLoopAt.eDegree_delete_add_two {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : (G.deleteEdges {e}).eDegree x + 2 = G.eDegree x

theorem Graph.IsLoopAt.degree_delete_add_two {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (h : G.IsLoopAt e x) : (G.deleteEdges {e}).degree x + 2 = G.degree x

theorem Graph.Inc.degree_delete_lt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} [G.LocallyFinite] (he : G.Inc e x) : (G.deleteEdges {e}).degree x < G.degree x

theorem Graph.IsLink.eDegree_delete_of_ne {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (hx : z ≠ x) (hy : z ≠ y) : (G.deleteEdges {e}).eDegree z = G.eDegree z

theorem Graph.IsLink.degree_delete_of_ne {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (hx : z ≠ x) (hy : z ≠ y) : (G.deleteEdges {e}).degree z = G.degree z

Trails

theorem Graph.IsTrail.eq_first_or_last_of_degree_eq_one {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {P : WList α β} (hP : G.IsTrail P) (hx : x ∈ P) (hdeg : G.IsLeaf x) : x = P.first ∨ x = P.last

theorem Graph.IsTrail.eq_first_or_last_of_eDegree_le_one {α : Type u_1} {β : Type u_2} {x : α} {G : Graph α β} {P : WList α β} (hP : G.IsTrail P) (hxP : x ∈ P) (hdeg : G.eDegree x ≤ 1) : x = P.first ∨ x = P.last

theorem Graph.IsTrail.disjoint_of_degree_le_one {α : Type u_1} {β : Type u_2} {G : Graph α β} {w : WList α β} {X : Set α} (hw : G.IsTrail w) (hX : ∀ x ∈ X, G.eDegree x ≤ 1) (hf : w.first ∉ X) (hl : w.last ∉ X) : Disjoint w.vertexSet X

Paths

theorem Graph.IsPath.first_isLeaf_toGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hne : P.Nonempty) : P.toGraph.IsLeaf P.first

theorem Graph.IsPath.last_isLeaf_toGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hne : P.Nonempty) : P.toGraph.IsLeaf P.last

theorem Graph.IsPath.eDegree_toGraph_eq_two {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hvP : v ∈ P) (hne_first : v ≠ P.first) (hne_last : v ≠ P.last) : P.toGraph.eDegree v = 2

theorem Graph.IsPath.degree_toGraph_eq_two {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β} {P : WList α β} (hP : G.IsPath P) (hvP : v ∈ P) (hne_first : v ≠ P.first) (hne_last : v ≠ P.last) : P.toGraph.degree v = 2

Cycles

theorem Graph.IsCyclicWalk.toGraph_regular {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.toGraph.Regular 2

Cycles are two-regular.