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.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.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