# Connectivity of subgraphs and induced graphs #

## Main definitions #

• SimpleGraph.Subgraph.Preconnected and SimpleGraph.Subgraph.Connected give subgraphs connectivity predicates via SimpleGraph.subgraph.coe.
structure SimpleGraph.Subgraph.Preconnected {V : Type u} {G : } (H : G.Subgraph) :

A subgraph is preconnected if it is preconnected when coerced to be a simple graph.

Note: This is a structure to make it so one can be precise about how dot notation resolves.

• coe : H.coe.Preconnected
Instances For
theorem SimpleGraph.Subgraph.Preconnected.coe {V : Type u} {G : } {H : G.Subgraph} (self : H.Preconnected) :
H.coe.Preconnected
instance SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe {V : Type u} {G : } {H : G.Subgraph} :
Coe H.Preconnected H.coe.Preconnected
Equations
• SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe = { coe := }
instance SimpleGraph.Subgraph.instCoeFunPreconnectedForallForallReachableElemVertsCoe {V : Type u} {G : } {H : G.Subgraph} :
CoeFun H.Preconnected fun (x : H.Preconnected) => ∀ (u v : H.verts), H.coe.Reachable u v
Equations
• SimpleGraph.Subgraph.instCoeFunPreconnectedForallForallReachableElemVertsCoe = { coe := }
theorem SimpleGraph.Subgraph.preconnected_iff {V : Type u} {G : } {H : G.Subgraph} :
H.Preconnected H.coe.Preconnected
structure SimpleGraph.Subgraph.Connected {V : Type u} {G : } (H : G.Subgraph) :

A subgraph is connected if it is connected when coerced to be a simple graph.

Note: This is a structure to make it so one can be precise about how dot notation resolves.

• coe : H.coe.Connected
Instances For
theorem SimpleGraph.Subgraph.Connected.coe {V : Type u} {G : } {H : G.Subgraph} (self : H.Connected) :
H.coe.Connected
instance SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe {V : Type u} {G : } {H : G.Subgraph} :
Coe H.Connected H.coe.Connected
Equations
• SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe = { coe := }
instance SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe {V : Type u} {G : } {H : G.Subgraph} :
CoeFun H.Connected fun (x : H.Connected) => ∀ (u v : H.verts), H.coe.Reachable u v
Equations
• SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe = { coe := }
theorem SimpleGraph.Subgraph.connected_iff' {V : Type u} {G : } {H : G.Subgraph} :
H.Connected H.coe.Connected
theorem SimpleGraph.Subgraph.connected_iff {V : Type u} {G : } {H : G.Subgraph} :
H.Connected H.Preconnected H.verts.Nonempty
theorem SimpleGraph.Subgraph.Connected.preconnected {V : Type u} {G : } {H : G.Subgraph} (h : H.Connected) :
H.Preconnected
theorem SimpleGraph.Subgraph.Connected.nonempty {V : Type u} {G : } {H : G.Subgraph} (h : H.Connected) :
H.verts.Nonempty
theorem SimpleGraph.Subgraph.singletonSubgraph_connected {V : Type u} {G : } {v : V} :
(G.singletonSubgraph v).Connected
@[simp]
theorem SimpleGraph.Subgraph.subgraphOfAdj_connected {V : Type u} {G : } {v : V} {w : V} (hvw : G.Adj v w) :
theorem SimpleGraph.Subgraph.top_induce_pair_connected_of_adj {V : Type u} {G : } {u : V} {v : V} (huv : G.Adj u v) :
(.induce {u, v}).Connected
theorem SimpleGraph.Subgraph.Connected.mono {V : Type u} {G : } {H : G.Subgraph} {H' : G.Subgraph} (hle : H H') (hv : H.verts = H'.verts) (h : H.Connected) :
H'.Connected
theorem SimpleGraph.Subgraph.Connected.mono' {V : Type u} {G : } {H : G.Subgraph} {H' : G.Subgraph} (hle : ∀ (v w : V), H.Adj v wH'.Adj v w) (hv : H.verts = H'.verts) (h : H.Connected) :
H'.Connected
theorem SimpleGraph.Subgraph.Connected.sup {V : Type u} {G : } {H : G.Subgraph} {K : G.Subgraph} (hH : H.Connected) (hK : K.Connected) (hn : (H K).verts.Nonempty) :
(H K).Connected
theorem SimpleGraph.Walk.toSubgraph_connected {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
p.toSubgraph.Connected
theorem SimpleGraph.Subgraph.induce_union_connected {V : Type u} {G : } {H : G.Subgraph} {s : Set V} {t : Set V} (sconn : (H.induce s).Connected) (tconn : (H.induce t).Connected) (sintert : (s t).Nonempty) :
(H.induce (s t)).Connected
theorem SimpleGraph.Subgraph.Connected.adj_union {V : Type u} {G : } {H : G.Subgraph} {K : G.Subgraph} (Hconn : H.Connected) (Kconn : K.Connected) {u : V} {v : V} (uH : u H.verts) (vK : v K.verts) (huv : G.Adj u v) :
(.induce {u, v} H K).Connected
theorem SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph {V : Type u} {G : } (H : G.Subgraph) :
H.Preconnected ∀ {u v : V}, u H.vertsv H.verts∃ (p : G.Walk u v), p.toSubgraph H
theorem SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph {V : Type u} {G : } (H : G.Subgraph) :
H.Connected H.verts.Nonempty ∀ {u v : V}, u H.vertsv H.verts∃ (p : G.Walk u v), p.toSubgraph H
theorem SimpleGraph.connected_induce_iff {V : Type u} {G : } {s : Set V} :
().Connected (.induce s).Connected
theorem SimpleGraph.induce_union_connected {V : Type u} {G : } {s : Set V} {t : Set V} (sconn : ().Connected) (tconn : ().Connected) (sintert : (s t).Nonempty) :
(SimpleGraph.induce (s t) G).Connected
theorem SimpleGraph.induce_pair_connected_of_adj {V : Type u} {G : } {u : V} {v : V} (huv : G.Adj u v) :
(SimpleGraph.induce {u, v} G).Connected
theorem SimpleGraph.Subgraph.Connected.induce_verts {V : Type u} {G : } {H : G.Subgraph} (h : H.Connected) :
(SimpleGraph.induce H.verts G).Connected
theorem SimpleGraph.Walk.connected_induce_support {V : Type u} {G : } {u : V} {v : V} (p : G.Walk u v) :
(SimpleGraph.induce {v_1 : V | v_1 p.support} G).Connected
theorem SimpleGraph.induce_connected_adj_union {V : Type u} {G : } {v : V} {w : V} {s : Set V} {t : Set V} (sconn : ().Connected) (tconn : ().Connected) (hv : v s) (hw : w t) (ha : G.Adj v w) :
(SimpleGraph.induce (s t) G).Connected
theorem SimpleGraph.induce_connected_of_patches {V : Type u} {G : } {s : Set V} (u : V) (hu : u s) (patches : ∀ {v : V}, v ss's, ∃ (hu' : u s') (hv' : v s'), ().Reachable u, hu' v, hv') :
().Connected
theorem SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint {V : Type u} {G : } {S : Set (Set V)} (Sn : S.Nonempty) (Snd : ∀ {s t : Set V}, s St S(s t).Nonempty) (Sc : ∀ {s : Set V}, s S().Connected) :
(SimpleGraph.induce (⋃₀ S) G).Connected
theorem SimpleGraph.extend_finset_to_connected {V : Type u} {G : } (Gpc : G.Preconnected) {t : } (tn : t.Nonempty) :
∃ (t' : ), t t' (SimpleGraph.induce (t') G).Connected