Connectivity of subgraphs and induced graphs #
Main definitions #
SimpleGraph.Subgraph.Preconnected
andSimpleGraph.Subgraph.Connected
give subgraphs connectivity predicates viaSimpleGraph.subgraph.coe
.
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 : 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
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 : 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.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
Instances For
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)
:
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)
:
theorem
SimpleGraph.Walk.mem_edges_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : G.Walk u v)
{e : Sym2 V}
:
@[simp]
theorem
SimpleGraph.Walk.edgeSet_toSubgraph
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : G.Walk u v)
:
@[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)
:
@[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)
:
theorem
SimpleGraph.Walk.toSubgraph_adj_getVert
{V : Type u}
{G : SimpleGraph V}
{u : V}
{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_iff
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
{u' : V}
{v' : V}
(w : G.Walk u v)
:
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)
:
theorem
SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph
{V : Type u}
{G : SimpleGraph V}
(H : G.Subgraph)
:
theorem
SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph
{V : Type u}
{G : SimpleGraph V}
(H : G.Subgraph)
:
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