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