theorem Graph.twoPaths {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsPath P) (hQ : G.IsPath Q) (hPQ : P ≠ Q) (h0 : P.first = Q.first) (h1 : P.last = Q.last) : ∃ (C : WList α β), G.IsCyclicWalk C ∧ C.edgeSet ⊆ P.edgeSet ∪ Q.edgeSet

If P and Q are distinct paths with the same ends, their union contains a cycle.

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

Equations

• G.IsForest = ∀ ⦃e : β⦄, e ∈ G.edgeSet → G.IsBridge e

theorem Graph.IsForest.isEdgeSep {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.IsForest) (he : e ∈ G.edgeSet) : G.IsEdgeSep {e}

theorem Graph.IsForest.isEdgeCutBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (hG : G.IsForest) (hl : G.IsLink e x y) : G.IsEdgeCutBetween {e} x y

theorem Graph.IsForest.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.IsForest) (hHG : H ≤ G) : H.IsForest

theorem Graph.IsForest.union_isForest_of_subsingleton_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.IsForest) (hH : H.IsForest) (hi : (G.vertexSet ∩ H.vertexSet).Subsingleton) : (G ∪ H).IsForest

The union of two forests that intersect in at most one vertex is a forest.

theorem Graph.IsForest.of_isCompOf_isForest {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : ∀ (H : Graph α β), H.IsCompOf G → H.IsForest) : G.IsForest

theorem Graph.IsPath.toGraph_isForest {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsPath P) : P.toGraph.IsForest

theorem Graph.IsCyclicWalk.toGraph_not_isForest {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : ¬C.toGraph.IsForest

theorem Graph.IsCyclicWalk.toGraph_eq_of_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {C C₀ : WList α β} (hC : G.IsCyclicWalk C) (hC₀ : G.IsCyclicWalk C₀) (hle : C₀.toGraph ≤ C.toGraph) : C₀.toGraph = C.toGraph

theorem Graph.IsForest.not_isTour {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsForest) : ¬G.IsTour P

theorem Graph.isForest_iff_not_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsForest ↔ ∀ (C : WList α β), ¬G.IsCyclicWalk C

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

Equations

• G.IsCycle = Minimal (fun (G : Graph α β) => ¬G.IsForest) G

theorem Graph.isCycle_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsCycle ↔ Minimal (fun (G : Graph α β) => ∃ e ∈ G.edgeSet, ¬G.IsBridge e) G

theorem Graph.IsCycle.isForest_of_lt {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.IsCycle) (hH : H < G) : H.IsForest

theorem Graph.IsCycle.edgeSet_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : G.edgeSet.Nonempty

theorem Graph.IsCycle.nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : G.vertexSet.Nonempty

theorem Graph.IsCycle.connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : G.Connected

theorem Graph.IsCyclicWalk.toGraph_isCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hC : G.IsCyclicWalk C) : C.toGraph.IsCycle

theorem Graph.IsCycle.exists_isCyclicWalk_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : ∃ (C : WList α β), G.IsCyclicWalk C ∧ C.toGraph = G

theorem Graph.isCycle_iff_exists_isCyclicWalk_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsCycle ↔ ∃ (C : WList α β), G.IsCyclicWalk C ∧ C.toGraph = G

theorem Graph.IsCycle.not_isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.IsCycle) : ¬G.IsBridge e

theorem Graph.IsLink.exists_cons_isCyclicWalk_eq_of_IsCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} {e : β} (hG : G.IsCycle) (hxy : G.IsLink e x y) : ∃ (C : WList α β), G.IsCyclicWalk (WList.cons x e C) ∧ C.first = y ∧ (WList.cons x e C).toGraph = G

Given a cycle and the 'orientation to traverse the cycle' in the form of a link, there exists a cyclic walk that starts with x, y.

theorem Graph.IsCycle.finite {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : G.Finite

theorem Graph.IsCycle.regular_two {α : Type u_1} {β : Type u_2} {C : Graph α β} (hC : C.IsCycle) : C.Regular 2

theorem Graph.IsCycle.three_le_encard_of_simple {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] (hG : G.IsCycle) : 3 ≤ G.vertexSet.encard

theorem Graph.IsCycle.connGE_two {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) (h3 : 3 ≤ G.vertexSet.encard) : G.ConnGE 2

A cycle on at least three vertices is 2-connected.

theorem Graph.IsCycle.eq_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.IsCycle) (hH : H.IsCycle) (hle : G ≤ H) : G = H

theorem Graph.IsCycle.toGraph_of_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {C : WList α β} (hG : G.IsCycle) (hC : G.IsCyclicWalk C) : C.toGraph = G

theorem Graph.IsCycle.loopless_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : G.Loopless ↔ G.vertexSet.Nontrivial

theorem Graph.IsCycle.simple_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsCycle) : G.Simple ↔ 3 ≤ G.vertexSet.encard

theorem Graph.IsCycle.exists_isCyclicWalk_of_vertex {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hG : G.IsCycle) (hx : x ∈ G.vertexSet) : ∃ (C : WList α β), G.IsCyclicWalk C ∧ C.first = x ∧ C.toGraph = G

Given a cycle and a vertex in the cycle, there exists a cyclic walk that starts with the vertex. The direction of the cyclic walk is not known.

theorem Graph.IsCycle.exists_isPath_isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hG : G.IsCycle) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) : ∃ (P : WList α β) (Q : WList α β), G.IsPath P ∧ G.IsTrail Q ∧ P.first = x ∧ P.last = y ∧ Q.first = y ∧ Q.last = x ∧ G.IsCyclicWalk (P ++ Q)

Without assuming x ≠ y, output maybe a trivial path and the entire cycle. See IsCycle.exists_two_paths_of_ne.

theorem Graph.IsCycle.exists_two_paths_of_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} (hG : G.IsCycle) (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) (hxy : x ≠ y) : ∃ (P : WList α β) (Q : WList α β), G.IsPath P ∧ G.IsPath Q ∧ P.first = x ∧ P.last = y ∧ Q.first = y ∧ Q.last = x ∧ G.IsCyclicWalk (P ++ Q)

theorem Graph.IsPath.isPrefix_of_isTrail_toGraph_of_first {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hP : G.IsPath P) (hQ : P.toGraph.IsTrail Q) (hfirst : Q.first = P.first) : Q.IsPrefix P

theorem WList.IsPrefix.isPrefix_of_isPrefix_of_length_le {α : Type u_1} {β : Type u_2} {w₁ w₂ P : WList α β} (h₁ : w₁.IsPrefix P) (h₂ : w₂.IsPrefix P) (hle : w₁.length ≤ w₂.length) : w₁.IsPrefix w₂

theorem Graph.IsCycle.isPrefix_of_isTrail_of_length_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} {w₁ w₂ : WList α β} (hG : G.IsCycle) (h₁ : G.IsTrail (WList.cons x e w₁)) (h₂ : G.IsTrail (WList.cons x e w₂)) (hle : w₁.length ≤ w₂.length) : w₁.IsPrefix w₂

theorem Graph.IsCycle.exists_isCyclicWalk_isPrefix_of_isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsCycle) (hP : G.IsTrail P) : ∃ (C : WList α β), G.IsCyclicWalk C ∧ P.IsPrefix C ∧ C.toGraph = G

theorem Graph.IsCycle.exists_path_of_exists_prop {α : Type u_1} {β : Type u_2} {G : Graph α β} {p q : α → Prop} (hG : G.IsCycle) (hp : ∃ x ∈ G.vertexSet, p x) (hq : ∃ x ∈ G.vertexSet, q x) : ∃ (P : WList α β), G.IsPath P ∧ p P.first ∧ q P.last ∧ (∀ x ∈ P.vertex.tail, ¬p x) ∧ ∀ x ∈ P.vertex.dropLast, ¬q x

theorem Graph.IsCycle.exists_compl_path_of_isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsCycle) (hP : G.IsTrail P) (hne : P.Nonempty) : ∃ (Q : WList α β), G.IsPath Q ∧ P.last = Q.first ∧ P.first = Q.last ∧ G.IsCyclicWalk (P ++ Q)

theorem Graph.IsCycle.exists_compl_path {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsCycle) (hP : G.IsPath P) (hne : P.Nonempty) : ∃ (Q : WList α β), G.IsPath Q ∧ Q.Nonempty ∧ P.last = Q.first ∧ P.first = Q.last ∧ G.IsCyclicWalk (P ++ Q)

theorem Graph.IsCycle.exists_compl_trail {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsCycle) (hP : G.IsTrail P) : ∃ (Q : WList α β), G.IsTrail Q ∧ P.last = Q.first ∧ P.first = Q.last ∧ G.IsCyclicWalk (P ++ Q)

@[simp]

theorem Graph.singleEdge_isForest {α : Type u_1} {β : Type u_2} {x y : α} (hxy : x ≠ y) (e : β) : (Graph.singleEdge x y e).IsForest

theorem Graph.IsForest.eq_of_isPath_eq_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hG : G.IsForest) (hP : G.IsPath P) (hQ : G.IsPath Q) (hfirst : P.first = Q.first) (hlast : P.last = Q.last) : P = Q

theorem Graph.IsForest.isPath_of_isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsForest) (hP : G.IsTrail P) : G.IsPath P

theorem Graph.IsForest.eq_of_isTrail_eq_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {P Q : WList α β} (hG : G.IsForest) (hP : G.IsTrail P) (hQ : G.IsTrail Q) (hfirst : P.first = Q.first) (hlast : P.last = Q.last) : P = Q

theorem Graph.isForest_of_minimal_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : Minimal (fun (F : Set β) => (G.restrict F).Connected) F) : (G.restrict F).IsForest

theorem Graph.IsForest.isShortestPath_of_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {P : WList α β} (hG : G.IsForest) (hP : G.IsPath P) : G.IsShortestPath P

theorem Graph.IsForest.loopless {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsForest) : G.Loopless

theorem Graph.IsForest.simple {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsForest) : G.Simple

theorem Graph.isForest_iff_isTrail_eq_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsForest ↔ ∀ ⦃P Q : WList α β⦄, G.IsTrail P → G.IsTrail Q → P.first = Q.first → P.last = Q.last → P = Q

theorem Graph.not_isForest_iff_exists_isCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} : ¬G.IsForest ↔ ∃ (H : Graph α β), H.IsCycle ∧ H ≤ G

theorem Graph.isForest_iff_not_isCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsForest ↔ ∀ H ≤ G, ¬H.IsCycle

Cycles and 2-connectivity

theorem Graph.ConnGE.exists_isCycle_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hG : G.ConnGE 2) (hx : x ∈ G.vertexSet) : ∃ (C₀ : Graph α β), C₀.IsCycle ∧ C₀ ≤ G ∧ x ∈ C₀.vertexSet ∧ 3 ≤ C₀.vertexSet.encard

A 2-connected graph has, through each of its vertices, a cycle on at least three vertices.

The bound on V(C) matters: IsCycle is Minimal (¬ IsForest ·), which admits loops and digons, and neither is 2-connected. No finiteness instance is needed: the cycle is built, not extracted.

theorem Graph.ConnGE.not_isForest {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.ConnGE 2) : ¬G.IsForest

theorem Graph.isCycle_iff_minimal_connGE_two {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Simple] : G.IsCycle ↔ Minimal (fun (x : Graph α β) => x.ConnGE 2) G

theorem Graph.IsForest.of_deleteEdges_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : G.IsBridge e) (hG : (G.deleteEdges {e}).IsForest) : G.IsForest

structure Graph.IsTree {α : Type u_1} {β : Type u_2} (T : Graph α β) : Prop

• isForest : T.IsForest
• connected : T.Connected

theorem Graph.isTree_iff {α : Type u_1} {β : Type u_2} (T : Graph α β) : T.IsTree ↔ T.IsForest ∧ T.Connected

theorem Graph.IsForest.isTree_of_IsCompOf {α : Type u_1} {β : Type u_2} {G T : Graph α β} (hG : G.IsForest) (hT : T.IsCompOf G) : T.IsTree

theorem Graph.IsTree.exists_delete_vertex_isTree {α : Type u_1} {β : Type u_2} {T : Graph α β} [T.Finite] (hT : T.IsTree) (hnt : T.vertexSet.Nontrivial) : ∃ v ∈ T.vertexSet, (T.deleteVerts {v}).IsTree

theorem Graph.IsLeaf.delete_isTree {α : Type u_1} {β : Type u_2} {T : Graph α β} {x : α} (hT : T.IsTree) (hx : T.IsLeaf x) : (T.deleteVerts {x}).IsTree

Leaves

theorem Graph.IsForest.exists_isPendant {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] (hG : G.IsForest) (hne : G.edgeSet.Nonempty) : ∃ (e : β) (x : α), G.IsPendant e x

Every forest with at least one edge has a pendant.

theorem Graph.IsForest.exists_isLeaf {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] (hG : G.IsForest) (hne : G.edgeSet.Nonempty) : ∃ (x : α), G.IsLeaf x

theorem Graph.IsTree.encard_vertexSet {α : Type u_1} {β : Type u_2} {T : Graph α β} (h : T.IsTree) : T.vertexSet.encard = T.edgeSet.encard + 1

theorem Graph.IsTree.ncard_vertexSet {α : Type u_1} {β : Type u_2} {T : Graph α β} [T.Finite] (h : T.IsTree) : T.vertexSet.ncard = T.edgeSet.ncard + 1

theorem Graph.IsForest.encard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsForest) : G.vertexSet.encard = G.edgeSet.encard + G.Components.encard

theorem Graph.IsForest.ncard_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hG : G.IsForest) : G.vertexSet.ncard = G.edgeSet.ncard + G.Components.ncard

theorem Graph.IsForest.encard_edgeSet_add_one_le {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.IsForest) (hne : G.vertexSet.Nonempty) : G.edgeSet.encard + 1 ≤ G.vertexSet.encard

theorem Graph.IsForest.ncard_edgeSet_lt {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hG : G.IsForest) (hne : G.vertexSet.Nonempty) : G.edgeSet.ncard < G.vertexSet.ncard