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

theorem SimpleGraph.Subgraph.Preconnected.coe {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (self : H.Preconnected) : 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

theorem SimpleGraph.Subgraph.Connected.coe {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (self : H.Connected) : 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 : 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 : V} (huv : G.Adj u v) : (⊤.induce {u, v}).Connected

theorem SimpleGraph.Subgraph.Connected.mono {V : Type u} {G : SimpleGraph V} {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 : SimpleGraph V} {H : G.Subgraph} {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 : G.Subgraph} {K : G.Subgraph} (hH : H.Connected) (hK : K.Connected) (hn : (H ⊓ K).verts.Nonempty) : (H ⊔ K).Connected

Walks as subgraphs

def SimpleGraph.Walk.toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {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 : V} (h : G.Adj u v) : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).toSubgraph = G.subgraphOfAdj h

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

theorem SimpleGraph.Walk.start_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {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 : 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 : 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 : 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 : 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} {v : 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 : 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 : 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 : V} (f : G →g G') (p : G.Walk u v) : (SimpleGraph.Walk.map f p).toSubgraph = SimpleGraph.Subgraph.map f p.toSubgraph

@[simp]

theorem SimpleGraph.Walk.finite_neighborSet_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : 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 : V} (p : G.Walk u v) : p.toSubgraph ≤ ⊤.induce {v_1 : V | v_1 ∈ p.support}

theorem SimpleGraph.Walk.toSubgraph_connected {V : Type u} {G : SimpleGraph V} {u : V} {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 : 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 : SimpleGraph V} {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 : 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} : (SimpleGraph.induce s G).Connected ↔ (⊤.induce s).Connected

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

theorem SimpleGraph.induce_pair_connected_of_adj {V : Type u} {G : SimpleGraph V} {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 : 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 : 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 : SimpleGraph V} {v : V} {w : V} {s : Set V} {t : Set V} (sconn : (SimpleGraph.induce s G).Connected) (tconn : (SimpleGraph.induce t G).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 : SimpleGraph V} {s : Set V} (u : V) (hu : u ∈ s) (patches : ∀ {v : V}, v ∈ s → ∃ s' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (SimpleGraph.induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩) : (SimpleGraph.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 → (SimpleGraph.induce s G).Connected) : (SimpleGraph.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' ∧ (SimpleGraph.induce (↑t') G).Connected