theorem Graph.IsCompOf.connected {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) : H.Connected

theorem Graph.IsCompOf.preconnected {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) : H.Preconnected

theorem Graph.walkable_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : (G.walkable x).Connected

@[simp]

theorem Graph.walkable_disjoint_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : α} : Disjoint (G.walkable x).vertexSet (G.walkable y).vertexSet ↔ ¬G.ConnBetween x y

theorem Graph.IsCompOf.eq_of_connBetween {α : Type u_1} {β : Type u_2} {G H₁ H₂ : Graph α β} {x y : α} (hH₁ : H₁.IsCompOf G) (hH₂ : H₂.IsCompOf G) (hxy : G.ConnBetween x y) (hx : x ∈ H₁.vertexSet) (hy : y ∈ H₂.vertexSet) : H₁ = H₂

theorem Graph.Preconnected.components_subsingleton {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Preconnected) : G.Components.Subsingleton

theorem Graph.components_subsingleton_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Components.Subsingleton ↔ G.Preconnected

@[simp]

theorem Graph.connPartition_rel_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : G.connPartition x y ↔ G.ConnBetween x y

theorem Graph.components_eq_singleton_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : (∃ (H : Graph α β), G.Components = {H}) ↔ G.Connected

@[simp]

theorem Graph.numberOfComponents_eq_one_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : c(G) = 1 ↔ G.Connected

theorem Graph.Connected.numberOfComponents {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Connected → c(G) = 1

Alias of the reverse direction of Graph.numberOfComponents_eq_one_iff.

theorem Graph.components_subsingleton_iff_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.Components.Subsingleton ↔ G = ⊥ ∨ G.Connected

theorem Graph.finite_components_of_finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] : G.Components.Finite

theorem Graph.ge_two_components_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (hNeBot : G.vertexSet.Nonempty) (h : ¬G.Connected) : 2 ≤ G.Components.encard

theorem Graph.not_connected_of_nontrivial_components {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Components.Nontrivial) : ¬G.Connected

theorem Graph.components_nontrivial_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (hNeBot : G.vertexSet.Nonempty) (h : ¬G.Connected) : G.Components.Nontrivial

theorem Graph.Connected.components_eq_singleton_self {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Connected) : G.Components = {G}

theorem Graph.components_eq_singleton_self {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Connected) : G.Components = {G}

theorem Graph.components_eq_singleton_self_iff {α : Type u_1} {β : Type u_2} {H : Graph α β} : H.Components = {H} ↔ H.Connected

theorem Graph.eq_iff_components_eq_components {α : Type u_1} {β : Type u_2} {G H : Graph α β} : G = H ↔ G.Components = H.Components

theorem Graph.IsCompOf.eq_of_connected {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsCompOf G) (hG : G.Connected) : H = G

theorem Graph.IsClosedSubgraph.isCompOf_of_isCompOf_compl {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h : H.IsClosedSubgraph G) (hK : K.IsCompOf G) : K.IsCompOf H ∨ K.IsCompOf (G.deleteVerts H.vertexSet)

theorem Graph.Connected.exists_isCompOf_ge {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.Connected) (hle : H ≤ G) : ∃ (G₁ : Graph α β), H ≤ G₁ ∧ G₁.IsCompOf G

theorem Graph.Connected.le_or_le_compl {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h : H.Connected) (hle : H ≤ G) (hK : K.IsClosedSubgraph G) : H ≤ K ∨ H ≤ G.deleteVerts K.vertexSet

theorem Graph.Connected.le_of_nonempty_inter {α : Type u_1} {β : Type u_2} {G H K : Graph α β} (h : H.Connected) (hle : H ≤ G) (hK : K.IsClosedSubgraph G) (hne : (H.vertexSet ∩ K.vertexSet).Nonempty) : H ≤ K

theorem Graph.isCompOf_iff_maximal {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsCompOf G ↔ Maximal (fun (K : Graph α β) => K.Connected ∧ K ≤ G) H

theorem Graph.Connected.union {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Connected) (hH : H.Connected) (hcompat : G.Compatible H) (hi : (H.vertexSet ∩ G.vertexSet).Nonempty) : (G ∪ H).Connected

theorem Graph.connected_union_iff_of_disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hV : Disjoint G.vertexSet H.vertexSet) : (G ∪ H).Connected ↔ G = ⊥ ∧ H.Connected ∨ G.Connected ∧ H = ⊥

theorem Graph.preconnected_union_iff_of_disjoint {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hV : Disjoint G.vertexSet H.vertexSet) : (G ∪ H).Preconnected ↔ G = ⊥ ∧ H.Preconnected ∨ G.Preconnected ∧ H = ⊥

theorem Graph.Connected.exists_inc_notMem_of_lt {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hG : G.Connected) (hlt : H < G) (hne : H.vertexSet.Nonempty) : ∃ (e : β) (x : α), G.Inc e x ∧ e ∉ H.edgeSet ∧ x ∈ H.vertexSet

@[simp]

theorem Graph.connected_bouquet {α : Type u_1} {β : Type u_2} (v : α) (F : Set β) : (bouquet v F).Connected

@[simp]

theorem Graph.connected_banana {α : Type u_1} {β : Type u_2} {F : Set β} (x y : α) (hF : F.Nonempty) : (banana x y F).Connected

@[simp]

theorem Graph.connected_singleEdge {α : Type u_1} {β : Type u_2} (x y : α) (e : β) : (Graph.singleEdge x y e).Connected

theorem Graph.Connected.addEdge_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} (hG : G.Connected) (hx : x ∈ G.vertexSet) (he : e ∉ G.edgeSet) (y : α) : (G.addEdge e x y).Connected

theorem Graph.walkable_eq_induce_setOf_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} : G.walkable x = G[{y : α | G.ConnBetween x y}]

theorem Graph.walkable_mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hle : G ≤ H) (x : α) : G.walkable x ≤ H.walkable x

theorem Graph.IsCompOf.of_deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} (hH : H.IsCompOf G) (hS : Disjoint H.vertexSet S) : H.IsCompOf (G.deleteVerts S)

theorem Graph.IsClosedSubgraph.vertexDelete_components_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsClosedSubgraph G) : (G.deleteVerts H.vertexSet).Components = G.Components \ H.Components

theorem Graph.IsClosedSubgraph.vertexDelete_components_encard_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsClosedSubgraph G) : (G.deleteVerts H.vertexSet).Components.encard + H.Components.encard = G.Components.encard

theorem Graph.IsCompOf.vertexDelete_components_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsCompOf G) : (G.deleteVerts H.vertexSet).Components = G.Components \ {H}

theorem Graph.IsCompOf.vertexDelete_components_encard_eq {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsCompOf G) : (G.deleteVerts H.vertexSet).Components.encard + 1 = G.Components.encard

theorem Graph.IsCompOf.isSepSet_of_three_le_components_encard {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.IsCompOf G) (hG : 3 ≤ G.Components.encard) : G.IsSep H.vertexSet

theorem Graph.IsCompOf.isSepSet_of_not_connected_of_ssubset {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} (hH : H.IsCompOf G) (hG : ¬G.Connected) (hssub : S ⊂ H.vertexSet) : G.IsSep S

theorem Graph.exists_isSepSet_with_encard_lt_components_encard {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : 3 ≤ G.vertexSet.encard) (hConn : ¬G.Connected) {n : ℕ∞} (hn : n + 2 ≤ G.vertexSet.encard) : ∃ (S : Set α), G.IsSep S ∧ S.encard = n

theorem Graph.exists_isSepSet_size_one_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : 3 ≤ G.vertexSet.encard) (h : ¬G.Connected) : ∃ (S : Set α), G.IsSep S ∧ S.encard = 1

theorem Graph.singleVertex_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hG : G.vertexSet = {x}) : G.Connected

theorem Graph.exists_of_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : ¬G.Connected) (hne : G.vertexSet.Nonempty) : ∃ X ⊂ G.vertexSet, X.Nonempty ∧ ∀ ⦃u v : α⦄, u ∈ X → G.Adj u v → v ∈ X

theorem Graph.connected_iff_forall_exists_adj {α : Type u_1} {β : Type u_2} {G : Graph α β} (hne : G.vertexSet.Nonempty) : G.Connected ↔ ∀ X ⊂ G.vertexSet, X.Nonempty → ∃ x ∈ X, ∃ y ∈ G.vertexSet \ X, G.Adj x y

theorem WList.WellFormed.toGraph_connected {α : Type u_1} {β : Type u_2} {W : WList α β} (hW : W.WellFormed) : W.toGraph.Connected

A WList that is WellFormed produces a connected graph.

theorem Graph.IsWalk.toGraph_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) : W.toGraph.Connected

theorem WList.WellFormed.toGraph_deleteVerts_singleton_connBetween_first_or_last {α : Type u_1} {β : Type u_2} {v x : α} {Q : WList α β} [DecidableEq α] (hQ : Q.WellFormed) (hQnd : List.count x Q.vertex ≤ 1) (hv : v ∈ Q) (hne : v ≠ x) : (Q.toGraph.deleteVerts {x}).ConnBetween v Q.first ∨ (Q.toGraph.deleteVerts {x}).ConnBetween v Q.last

theorem Graph.Preconnected.exists_connBetween_deleteEdge_set {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {X : Set α} (hG : G.Preconnected) (hX : (X ∩ G.vertexSet).Nonempty) (hu : u ∈ G.vertexSet) : ∃ x ∈ X, (G.deleteEdges G[X].edgeSet).ConnBetween u x

theorem Graph.Preconnected.exists_isPathFrom {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (hG : G.Preconnected) (hS : (S ∩ G.vertexSet).Nonempty) (hT : (T ∩ G.vertexSet).Nonempty) : ∃ (P : WList α β), G.IsPathFrom S T P

theorem Graph.Preconnected.exists_connBetween_deleteEdge_set_set {α : Type u_1} {β : Type u_2} {G : Graph α β} {S T : Set α} (hG : G.Preconnected) (hS : (S ∩ G.vertexSet).Nonempty) (hT : (T ∩ G.vertexSet).Nonempty) : ∃ x ∈ S, ∃ y ∈ T, (G.deleteEdges (G[S].edgeSet ∪ G[T].edgeSet)).ConnBetween x y

theorem Graph.loopRemove_preconnected_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.loopRemove.Preconnected ↔ G.Preconnected

theorem Graph.loopRemove_connected_iff {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.loopRemove.Connected ↔ G.Connected

theorem Graph.deleteEdges_connected_iff_of_forall_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hF : ∀ e ∈ F, ∃ (x : α), G.IsLoopAt e x) : (G.deleteEdges F).Connected ↔ G.Connected

theorem Graph.deleteEdges_isLoopAt_isSep_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (C : Set α) : (G.deleteEdges E(G, u, u)).IsSep C ↔ G.IsSep C

theorem Graph.Preconnected.deleteEdges_linkEdges_connBetween_or {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} (hG : G.Preconnected) (hx : x ∈ G.vertexSet) (hu : u ∈ G.vertexSet) (hv : v ∈ G.vertexSet) : (G.deleteEdges E(G, u, v)).ConnBetween x u ∨ (G.deleteEdges E(G, u, v)).ConnBetween x v

theorem Graph.Preconnected.deleteEdges_linkEdges_not_connBetween {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (hG : G.Preconnected) (h' : ¬(G.deleteEdges E(G, u, v)).Preconnected) : ¬(G.deleteEdges E(G, u, v)).ConnBetween u v

theorem Graph.Preconnected.deleteEdges_linkEdges_components {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (hG : G.Preconnected) (hu : u ∈ G.vertexSet) (hv : v ∈ G.vertexSet) : (G.deleteEdges E(G, u, v)).Components = {(G.deleteEdges E(G, u, v)).walkable u, (G.deleteEdges E(G, u, v)).walkable v}

theorem Graph.Preconnected.walkable_singleton_left_of_deleteVerts_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (hG : G.Preconnected) (h : ¬(G.deleteEdges E(G, u, v)).Connected) (huconn : (G.deleteVerts {u}).Connected) : ((G.deleteEdges E(G, u, v)).walkable u).vertexSet = {u}

theorem Graph.Preconnected.walkable_singleton_right_of_deleteVerts_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (hG : G.Preconnected) (h : ¬(G.deleteEdges E(G, u, v)).Connected) (hvconn : (G.deleteVerts {v}).Connected) : ((G.deleteEdges E(G, u, v)).walkable v).vertexSet = {v}

theorem Graph.not_connected_or_singleton_isSep_or_pair {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : ¬(G.deleteEdges E(G, u, v)).Connected) : ¬G.Connected ∨ G.IsSep {u} ∨ G.IsSep {v} ∨ G.vertexSet = {u, v}

theorem Graph.not_preconnected_or_singleton_isSep_or_pair {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : ¬(G.deleteEdges E(G, u, v)).Preconnected) : ¬G.Preconnected ∨ G.IsSep {u} ∨ G.IsSep {v} ∨ G.vertexSet = {u, v}

theorem Graph.IsSep.of_deleteEdges_linkEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {S : Set α} (h : (G.deleteEdges E(G, u, v)).IsSep S) : G.IsSep S ∨ G.IsSep (insert u S) ∨ G.IsSep (insert v S) ∨ G.vertexSet = {u, v} ∪ S

theorem Graph.ConnGE.deleteEdges_linkEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (h : G.ConnGE (n + 1)) (u v : α) : (G.deleteEdges E(G, u, v)).ConnGE n

theorem Graph.Preconnected.exists_isLink_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (h : G.Preconnected) (hV : G.vertexSet.Nontrivial) (hx : x ∈ G.vertexSet) : ∃ (e : β) (y : α), G.IsLink e x y ∧ y ≠ x

theorem Graph.Connected.exists_isLink_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hG : G.Connected) (hV : G.vertexSet.Nontrivial) (hx : x ∈ G.vertexSet) : ∃ (e : β) (y : α), G.IsLink e x y ∧ y ≠ x

theorem Graph.Isolated.not_preconnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : G.Isolated x) (hnt : G.vertexSet.Nontrivial) : ¬G.Preconnected

theorem Graph.Isolated.not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} (hx : G.Isolated x) (hnt : G.vertexSet.Nontrivial) : ¬G.Connected

theorem Graph.Preconnected.degreePos {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Preconnected) (hnt : G.vertexSet.Nontrivial) : G.DegreePos

theorem Graph.Connected.degreePos {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Connected) (hnt : G.vertexSet.Nontrivial) : G.DegreePos

theorem Graph.Connected.edgeSet_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.Connected) (hnt : G.vertexSet.Nontrivial) : G.edgeSet.Nonempty

theorem Graph.Preconnected.finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] (h : G.Preconnected) : G.Finite

theorem Graph.Connected.finite {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.EdgeFinite] (h : G.Connected) : G.Finite

theorem Graph.Connected.exists_of_restrict_not_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β} (hG : G.Connected) (hF : ¬(G.restrict F).Connected) : ∃ (S : (G.restrict F).Separation) (e : β) (x : α) (y : α), e ∉ F ∧ x ∈ S.left ∧ y ∈ S.right ∧ G.IsLink e x y

If G is connected but its restriction to some set F of edges is not, then there is an edge of G joining two vertices that are not connected in the restriction.

theorem Graph.IsSep.exists_adj_of_isCompOf_deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} {S : Set α} (hM : G.IsSep S) (hG : G.Connected) (hH : H.IsCompOf (G.deleteVerts S)) : ∃ x ∈ S, ∃ y ∈ H.vertexSet, G.Adj x y

theorem Graph.IsMinSep.exists_adj_of_isCompOf_deleteVerts {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x : α} {S : Set α} (hM : G.IsMinSep S) (hH : H.IsCompOf (G.deleteVerts S)) (hx : x ∈ S) (hfin : S.Finite) : ∃ y ∈ H.vertexSet, G.Adj x y

Every vertex in a mininum cardinality separator has an edge to components of the vertex-deleted graph. This lemma requires the separator to be finite because IsMinSep uses encard for cardinality comparison and cannot tell the size difference of infinite sets.

theorem Graph.ConnGE.connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {n : ℕ} (hG : G.ConnGE n) (hn : 1 ≤ n) : G.Connected

theorem Graph.Preconnected.exists_isNonloopAt_of_nontrivial {α : Type u_1} {β : Type u_2} {G : Graph α β} (hG : G.Preconnected) (hnt : G.vertexSet.Nontrivial) : ∃ (e : β) (x : α), G.IsNonloopAt e x

theorem Graph.ConnGE.exists_isNonloopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {k : ℕ} (hG : G.ConnGE k) (hk : 2 ≤ k) : ∃ (e : β) (x : α), G.IsNonloopAt e x

theorem Graph.Compatible.union_connected_of_forall {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (hG : G.Connected) (hH : ∀ x ∈ H.vertexSet, ∃ y ∈ G.vertexSet, H.ConnBetween x y) : (G ∪ H).Connected

theorem Graph.Compatible.union_connected_of_nonempty_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : G.Compatible H) (hG : G.Connected) (hH : H.Connected) (hne : (G.vertexSet ∩ H.vertexSet).Nonempty) : (G ∪ H).Connected

theorem Graph.IsWalk.exists_mem_mem_of_union {α : Type u_1} {β : Type u_2} {G H : Graph α β} {x y : α} {W : WList α β} (h : (G ∪ H).IsWalk W) (hxW : x ∈ W.vertexSet) (hyW : y ∈ W.vertexSet) (hxG : x ∈ G.vertexSet) (hyH : y ∈ H.vertexSet) : ∃ x ∈ W, x ∈ G.vertexSet ∧ x ∈ H.vertexSet

theorem Graph.union_not_connected_of_disjoint_vertexSet {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hV : Disjoint G.vertexSet H.vertexSet) (hG : G.vertexSet.Nonempty) (hH : H.vertexSet.Nonempty) : ¬(G ∪ H).Connected

theorem Graph.IsPath.isPath_of_union_of_subsingleton_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} {P : WList α β} (hP : (G ∪ H).IsPath P) (hi : (G.vertexSet ∩ H.vertexSet).Subsingleton) (hf : P.first ∈ G.vertexSet) (hl : P.last ∈ G.vertexSet) : G.IsPath P

Cycles

theorem Graph.IsCyclicWalk.connBetween_deleteVertex_of_mem_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {y₁ y₂ : α} {C : WList α β} (hC : G.IsCyclicWalk C) (x : α) (hy₁ : y₁ ∈ C) (hy₂ : y₂ ∈ C) (hne₁ : y₁ ≠ x) (hne₂ : y₂ ≠ x) : (G.deleteVerts {x}).ConnBetween y₁ y₂

Two vertices of a cycle are connected after deleting any other vertex.

theorem Graph.IsCyclicWalk.connBetween_deleteEdge_of_mem_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x₁ x₂ : α} {C : WList α β} (hC : G.IsCyclicWalk C) (e : β) (hx₁ : x₁ ∈ C) (hx₂ : x₂ ∈ C) : (G.deleteEdges {e}).ConnBetween x₁ x₂

Two vertices of a cycle are connected after deleting any edge.

theorem Graph.IsCyclicWalk.isCyclicWalk_or_isCyclicWalk_of_union_of_subsingleton_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : WList α β} (hC : (G ∪ H).IsCyclicWalk C) (hi : (G.vertexSet ∩ H.vertexSet).Subsingleton) : G.IsCyclicWalk C ∨ H.IsCyclicWalk C

If two graphs intersect in at most one vertex, then any cycle of their union is a cycle of one of the graphs.

theorem Graph.Compatible.isCyclicWalk_union_iff_of_subsingleton_inter {α : Type u_1} {β : Type u_2} {G H : Graph α β} {C : WList α β} (hcompat : G.Compatible H) (hi : (G.vertexSet ∩ H.vertexSet).Subsingleton) : (G ∪ H).IsCyclicWalk C ↔ G.IsCyclicWalk C ∨ H.IsCyclicWalk C

theorem Graph.Connected.exists_component_ge {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.Connected) (hle : H ≤ G) : ∃ (G₁ : Graph α β), G₁.IsCompOf G ∧ H ≤ G₁

Every connected subgraph of G is a subgraph of a component of G.

theorem Graph.exists_IsCompOf_edge_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (he : e ∈ G.edgeSet) : ∃ (H : Graph α β), H.IsCompOf G ∧ e ∈ H.edgeSet

theorem Graph.IsWalk.exists_IsCompOf_isWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {W : WList α β} (hW : G.IsWalk W) : ∃ (H : Graph α β), H.IsCompOf G ∧ H.IsWalk W

theorem Graph.IsCompOf_iff_isClosedSubgraph_connected {α : Type u_1} {β : Type u_2} {G H : Graph α β} : H.IsCompOf G ↔ H.IsClosedSubgraph G ∧ H.Connected

theorem Graph.IsClosedSubgraph.isCompOf_of_connected {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsClosedSubgraph G) (hH : H.Connected) : H.IsCompOf G

theorem Graph.Connected.isCompOf_of_isClosedSubgraph {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.Connected) (h : H.IsClosedSubgraph G) : H.IsCompOf G

def Graph.IsCompOf.separation_of_ne {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) (hne : H ≠ G) : G.Separation

For a proper component H, the separation with parts V(H) and V(G) \ V(H).

Equations

• h.separation_of_ne hne = { left := H.vertexSet, right := G.vertexSet \ H.vertexSet, nonempty_left := ⋯, nonempty_right := ⋯, disjoint := ⋯, union_eq := ⋯, not_adj := ⋯ }

@[simp]

theorem Graph.IsCompOf.separation_of_ne_right {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) (hne : H ≠ G) : (h.separation_of_ne hne).right = G.vertexSet \ H.vertexSet

@[simp]

theorem Graph.IsCompOf.separation_of_ne_left {α : Type u_1} {β : Type u_2} {G H : Graph α β} (h : H.IsCompOf G) (hne : H ≠ G) : (h.separation_of_ne hne).left = H.vertexSet

theorem Graph.Connected.exists_separation_of_le {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hH : H.Connected) (hG : ¬G.Connected) (hle : H ≤ G) : ∃ (S : G.Separation), H ≤ G[S.left]

If H is a connected subgraph of a disconnected graph G, then there is a separation of G with H on the left.

theorem Graph.IsCompOf_sUnion_iff {α : Type u_1} {β : Type u_2} {H : Graph α β} {s : Set (Graph α β)} (h : s.Pairwise StronglyDisjoint) (hs : ∀ G ∈ s, G.Connected) : H.IsCompOf (Graph.sUnion s ⋯) ↔ H ∈ s

The components of the union of a set of disjoint connected graphs are the graphs themselves.

theorem Graph.Connected.eq_of_le_of_forall_degree_ge {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.LocallyFinite] (hG : G.Connected) (hle : H ≤ G) (hne : H.vertexSet.Nonempty) (hdeg : ∀ ⦃x : α⦄, x ∈ H.vertexSet → G.degree x ≤ H.degree x) : H = G

If H is a nonempty subgraph of a connected graph G, and each vertex degree in H is at least the corresponding degree in G, then H = G.

theorem Graph.regular_sUnion_iff {α : Type u_1} {β : Type u_2} {s : Set (Graph α β)} (hdj : s.Pairwise StronglyDisjoint) {d : ℕ} : (Graph.sUnion s ⋯).Regular d ↔ ∀ G ∈ s, G.Regular d

theorem Graph.regular_iff_forall_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} : G.Regular d ↔ ∀ (H : Graph α β), H.IsCompOf G → H.Regular d

theorem Graph.maxDegreeLE_iff_forall_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {d : ℕ} : G.MaxDegreeLE d ↔ ∀ (H : Graph α β), H.IsCompOf G → H.MaxDegreeLE d

@[simp]

theorem Graph.noEdge_isComplete_iff {α : Type u_1} {β : Type u_2} {X : Set α} : (noEdge X β).IsComplete ↔ X.Subsingleton

@[simp]

theorem Graph.IsWalk.nil_of_noEdge {α : Type u_1} {β : Type u_2} {W : WList α β} {X : Set α} (h : (noEdge X β).IsWalk W) : W.Nil

@[simp]

theorem Graph.connBetween_noEdge_iff {α : Type u_1} {β : Type u_2} {x y : α} {X : Set α} : (noEdge X β).ConnBetween x y ↔ x = y ∧ x ∈ X

@[simp]

theorem Graph.noEdge_preconnected_iff {α : Type u_1} {β : Type u_2} {X : Set α} : (noEdge X β).Preconnected ↔ X.Subsingleton

@[simp]

theorem Graph.noEdge_connected_iff {α : Type u_1} {β : Type u_2} {X : Set α} : (noEdge X β).Connected ↔ ∃ (v : α), X = {v}

@[simp]

theorem Graph.IsSepBetween.ne_of_noEdge {α : Type u_1} {β : Type u_2} {x y : α} {X Y : Set α} (h : (noEdge X β).IsSepBetween x y Y) (hx : x ∈ X) : x ≠ y

theorem Graph.isSepBetween_noEdge_of_ne {α : Type u_1} {β : Type u_2} {x y : α} {X Y : Set α} (hne : x ≠ y) (hY : Y ⊆ X \ {x, y}) : (noEdge X β).IsSepBetween x y Y

@[simp]

theorem Graph.isEdgeSep_noEdge_iff {α : Type u_1} {β : Type u_2} {F : Set β} {X : Set α} : (noEdge X β).IsEdgeSep F ↔ F = ∅ ∧ X.encard ≠ 1

@[simp]

theorem Graph.isEdgeSep_bot_iff {α : Type u_1} {β : Type u_2} {F : Set β} : ⊥.IsEdgeSep F ↔ F = ∅

@[simp]

theorem Graph.noEdge_connBetweenGE_iff {α : Type u_1} {β : Type u_2} {x y : α} {X : Set α} (n : ℕ) : (noEdge X β).ConnBetweenGE x y n ↔ n = 0 ∨ x = y ∧ x ∈ X

@[simp]

theorem Graph.noEdge_preconnGE_iff {α : Type u_1} {β : Type u_2} {X : Set α} (n : ℕ) : (noEdge X β).PreconnGE n ↔ n = 0 ∨ X.Subsingleton

@[simp]

theorem Graph.noEdge_ConnGE_iff {α : Type u_1} {β : Type u_2} {X : Set α} (n : ℕ) : (noEdge X β).ConnGE n ↔ n = 0 ∨ n = 1 ∧ ∃ (x : α), X = {x}