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 : SimpleGraph V} (H : G.Subgraph) : Prop

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

instance SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : Coe H.Preconnected H.coe.Preconnected

Equations

• SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe = { coe := ⋯ }

instance SimpleGraph.Subgraph.instCoeFunPreconnectedForallForallReachableElemVertsCoe {V : Type u} {G : SimpleGraph V} {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 : SimpleGraph V} {H : G.Subgraph} : H.Preconnected ↔ H.coe.Preconnected

structure SimpleGraph.Subgraph.Connected {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) : Prop

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

instance SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : Coe H.Connected H.coe.Connected

Equations

• SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe = { coe := ⋯ }

instance SimpleGraph.Subgraph.instCoeFunConnectedForallForallReachableElemVertsCoe {V : Type u} {G : SimpleGraph V} {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 : SimpleGraph V} {H : G.Subgraph} : H.Connected ↔ H.coe.Connected

theorem SimpleGraph.Subgraph.connected_iff {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} : H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty

theorem SimpleGraph.Subgraph.Connected.preconnected {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (h : H.Connected) : H.Preconnected

theorem SimpleGraph.Subgraph.Connected.nonempty {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (h : H.Connected) : H.verts.Nonempty

theorem SimpleGraph.Subgraph.singletonSubgraph_connected {V : Type u} {G : SimpleGraph V} {v : V} : (G.singletonSubgraph v).Connected

@[simp]

theorem SimpleGraph.Subgraph.subgraphOfAdj_connected {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w) : (G.subgraphOfAdj hvw).Connected

theorem SimpleGraph.Subgraph.top_induce_pair_connected_of_adj {V : Type u} {G : SimpleGraph V} {u v : V} (huv : G.Adj u v) : (⊤.induce {u, v}).Connected

theorem SimpleGraph.Subgraph.Connected.mono {V : Type u} {G : SimpleGraph V} {H 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 : SimpleGraph V} {H H' : G.Subgraph} (hle : ∀ (v w : V), H.Adj v w → H'.Adj v w) (hv : H.verts = H'.verts) (h : H.Connected) : H'.Connected

theorem SimpleGraph.Subgraph.Connected.sup {V : Type u} {G : SimpleGraph V} {H K : G.Subgraph} (hH : H.Connected) (hK : K.Connected) (hn : (H ⊓ K).verts.Nonempty) : (H ⊔ K).Connected

theorem SimpleGraph.Subgraph.Connected.exists_verts_eq_connectedComponentSupp {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (hc : H.Connected) (h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w) : ∃ (c : G.ConnectedComponent), H.verts = c.supp

This lemma establishes a condition under which a subgraph is the same as a connected component. Note the asymmetry in the hypothesis h: v is in H.verts, but w is not required to be.

Walks as subgraphs

def SimpleGraph.Walk.toSubgraph {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → G.Subgraph

The subgraph consisting of the vertices and edges of the walk.

Equations

• SimpleGraph.Walk.nil.toSubgraph = G.singletonSubgraph u
• (SimpleGraph.Walk.cons h p).toSubgraph = G.subgraphOfAdj h ⊔ p.toSubgraph

theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v) : (cons h nil).toSubgraph = G.subgraphOfAdj h

theorem SimpleGraph.Walk.mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) : w ∈ p.toSubgraph.verts ↔ w ∈ p.support

theorem SimpleGraph.Walk.not_nil_of_adj_toSubgraph {V : Type u} {G : SimpleGraph V} {w u v x : V} {p : G.Walk u v} (hadj : p.toSubgraph.Adj w x) : ¬p.Nil

theorem SimpleGraph.Walk.start_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : u ∈ p.toSubgraph.verts

theorem SimpleGraph.Walk.end_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : v ∈ p.toSubgraph.verts

@[simp]

theorem SimpleGraph.Walk.verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toSubgraph.verts = {w : V | w ∈ p.support}

theorem SimpleGraph.Walk.mem_edges_toSubgraph {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {e : Sym2 V} : e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

@[simp]

theorem SimpleGraph.Walk.edgeSet_toSubgraph {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toSubgraph.edgeSet = {e : Sym2 V | e ∈ p.edges}

@[simp]

theorem SimpleGraph.Walk.toSubgraph_append {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph

@[simp]

theorem SimpleGraph.Walk.toSubgraph_reverse {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.reverse.toSubgraph = p.toSubgraph

@[simp]

theorem SimpleGraph.Walk.toSubgraph_rotate {V : Type u} {G : SimpleGraph V} {u v : V} [DecidableEq V] (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).toSubgraph = c.toSubgraph

@[simp]

theorem SimpleGraph.Walk.toSubgraph_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u v : V} (f : G →g G') (p : G.Walk u v) : (Walk.map f p).toSubgraph = Subgraph.map f p.toSubgraph

theorem SimpleGraph.Walk.adj_toSubgraph_mapLe {V : Type u} {G : SimpleGraph V} {u v : V} {G' : SimpleGraph V} {w x : V} {p : G.Walk u v} (h : G ≤ G') : (mapLe h p).toSubgraph.Adj w x ↔ p.toSubgraph.Adj w x

@[simp]

theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) : (p.toSubgraph.neighborSet w).Finite

theorem SimpleGraph.Walk.toSubgraph_le_induce_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toSubgraph ≤ ⊤.induce {v_1 : V | v_1 ∈ p.support}

theorem SimpleGraph.Walk.toSubgraph_adj_getVert {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) : w.toSubgraph.Adj (w.getVert i) (w.getVert (i + 1))

theorem SimpleGraph.Walk.toSubgraph_adj_snd {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj u w.snd

theorem SimpleGraph.Walk.toSubgraph_adj_penultimate {V : Type u} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) (h : ¬w.Nil) : w.toSubgraph.Adj w.penultimate v

theorem SimpleGraph.Walk.toSubgraph_adj_iff {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (w : G.Walk u v) : w.toSubgraph.Adj u' v' ↔ ∃ (i : ℕ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') ∧ i < w.length

theorem SimpleGraph.Walk.mem_support_of_adj_toSubgraph {V : Type u} {G : SimpleGraph V} {u v u' v' : V} {p : G.Walk u v} (hp : p.toSubgraph.Adj u' v') : u' ∈ p.support

theorem SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_startpoint {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (hnp : ¬p.Nil) : p.toSubgraph.neighborSet u = {p.snd}

theorem SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_endpoint {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} (hp : p.IsPath) (hnp : ¬p.Nil) : p.toSubgraph.neighborSet v = {p.penultimate}

theorem SimpleGraph.Walk.IsPath.neighborSet_toSubgraph_internal {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath) (h : i ≠ 0) (h' : i < p.length) : p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

theorem SimpleGraph.Walk.IsPath.ncard_neighborSet_toSubgraph_internal_eq_two {V : Type u} {G : SimpleGraph V} {v u : V} {i : ℕ} {p : G.Walk u v} (hp : p.IsPath) (h : i ≠ 0) (h' : i < p.length) : (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

theorem SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj {V : Type u} {G : SimpleGraph V} {u v v' : V} {p : G.Walk u v} (hp : p.IsPath) (hadj : p.toSubgraph.Adj u v') : p.snd = v'

theorem SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_endpoint {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (hpc : p.IsCycle) : p.toSubgraph.neighborSet u = {p.snd, p.penultimate}

theorem SimpleGraph.Walk.IsCycle.neighborSet_toSubgraph_internal {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u} (hpc : p.IsCycle) (h : i ≠ 0) (h' : i < p.length) : p.toSubgraph.neighborSet (p.getVert i) = {p.getVert (i - 1), p.getVert (i + 1)}

theorem SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u u} (hpc : p.IsCycle) (h : v ∈ p.support) : (p.toSubgraph.neighborSet v).ncard = 2

theorem SimpleGraph.Walk.IsCycle.exists_isCycle_snd_verts_eq {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v v} (h : p.IsCycle) (hadj : p.toSubgraph.Adj v w) : ∃ (p' : G.Walk v v), p'.IsCycle ∧ p'.snd = w ∧ p'.toSubgraph.verts = p.toSubgraph.verts

theorem SimpleGraph.Walk.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) : ∃ x ∈ s, ∃ (hx : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅

This lemma states that given some finite set of vertices, of which at least one is in the support of a given walk, one of them is the first to be encountered. This consequence is encoded as the set of vertices, restricted to those in the support, except for the first, being empty. You could interpret this as being takeUntilSet, but defining this is slightly involved due to not knowing what the final vertex is. This could be done by defining a function to obtain the first encountered vertex and then use that to define takeUntilSet. That direction could be worthwhile if this concept is used more widely.

theorem SimpleGraph.Walk.exists_mem_support_forall_mem_support_imp_eq {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} {p : G.Walk u v} (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) : ∃ x ∈ s, ∃ (hx : x ∈ p.support), ∀ t ∈ s, t ∈ (p.takeUntil x hx).support → t = x

theorem SimpleGraph.Walk.toSubgraph_connected {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toSubgraph.Connected

theorem SimpleGraph.Subgraph.induce_union_connected {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {s 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 : SimpleGraph V} {H K : G.Subgraph} (Hconn : H.Connected) (Kconn : K.Connected) {u 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 : SimpleGraph V} (H : G.Subgraph) : H.Preconnected ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H

theorem SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) : H.Connected ↔ H.verts.Nonempty ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ (p : G.Walk u v), p.toSubgraph ≤ H

theorem SimpleGraph.connected_induce_iff {V : Type u} {G : SimpleGraph V} {s : Set V} : (induce s G).Connected ↔ (⊤.induce s).Connected

theorem SimpleGraph.induce_union_connected {V : Type u} {G : SimpleGraph V} {s t : Set V} (sconn : (induce s G).Connected) (tconn : (induce t G).Connected) (sintert : (s ∩ t).Nonempty) : (induce (s ∪ t) G).Connected

theorem SimpleGraph.induce_pair_connected_of_adj {V : Type u} {G : SimpleGraph V} {u v : V} (huv : G.Adj u v) : (induce {u, v} G).Connected

theorem SimpleGraph.Subgraph.Connected.induce_verts {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (h : H.Connected) : (SimpleGraph.induce H.verts G).Connected

theorem SimpleGraph.Walk.connected_induce_support {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : (induce {v_1 : V | v_1 ∈ p.support} G).Connected

theorem SimpleGraph.induce_connected_adj_union {V : Type u} {G : SimpleGraph V} {v w : V} {s t : Set V} (sconn : (induce s G).Connected) (tconn : (induce t G).Connected) (hv : v ∈ s) (hw : w ∈ t) (ha : G.Adj v w) : (induce (s ∪ t) G).Connected

theorem SimpleGraph.induce_connected_of_patches {V : Type u} {G : SimpleGraph V} {s : Set V} (u : V) (hu : u ∈ s) (patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩) : (induce s G).Connected

theorem SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint {V : Type u} {G : SimpleGraph V} {S : Set (Set V)} (Sn : S.Nonempty) (Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty) (Sc : ∀ {s : Set V}, s ∈ S → (induce s G).Connected) : (induce (⋃₀ S) G).Connected

theorem SimpleGraph.extend_finset_to_connected {V : Type u} {G : SimpleGraph V} (Gpc : G.Preconnected) {t : Finset V} (tn : t.Nonempty) : ∃ (t' : Finset V), t ⊆ t' ∧ (induce (↑t') G).Connected