Connectivity of subgraphs and induced graphs #
Main definitions #
SimpleGraph.Subgraph.Preconnected
andSimpleGraph.Subgraph.Connected
give subgraphs connectivity predicates viaSimpleGraph.subgraph.coe
.
structure
SimpleGraph.Subgraph.Preconnected
{V : Type u}
{G : SimpleGraph V}
(H : SimpleGraph.Subgraph G)
:
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.
Instances For
instance
SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
instance
SimpleGraph.Subgraph.instCoeFunPreconnectedForAllElemVertsReachableCoe
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
CoeFun (SimpleGraph.Subgraph.Preconnected H) fun x =>
∀ (u v : ↑H.verts), SimpleGraph.Reachable (SimpleGraph.Subgraph.coe H) u v
theorem
SimpleGraph.Subgraph.preconnected_iff
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
structure
SimpleGraph.Subgraph.Connected
{V : Type u}
{G : SimpleGraph V}
(H : SimpleGraph.Subgraph G)
:
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.
Instances For
instance
SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
instance
SimpleGraph.Subgraph.instCoeFunConnectedForAllElemVertsReachableCoe
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
CoeFun (SimpleGraph.Subgraph.Connected H) fun x =>
∀ (u v : ↑H.verts), SimpleGraph.Reachable (SimpleGraph.Subgraph.coe H) u v
theorem
SimpleGraph.Subgraph.connected_iff'
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
theorem
SimpleGraph.Subgraph.connected_iff
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
:
theorem
SimpleGraph.Subgraph.Connected.preconnected
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
(h : SimpleGraph.Subgraph.Connected H)
:
theorem
SimpleGraph.Subgraph.Connected.nonempty
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
(h : SimpleGraph.Subgraph.Connected H)
:
Set.Nonempty H.verts
@[simp]
theorem
SimpleGraph.Subgraph.subgraphOfAdj_connected
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
(hvw : SimpleGraph.Adj G v w)
:
theorem
SimpleGraph.Subgraph.top_induce_pair_connected_of_adj
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(huv : SimpleGraph.Adj G u v)
:
theorem
SimpleGraph.Subgraph.Connected.mono
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
{H' : SimpleGraph.Subgraph G}
(hle : H ≤ H')
(hv : H.verts = H'.verts)
(h : SimpleGraph.Subgraph.Connected H)
:
theorem
SimpleGraph.Subgraph.Connected.mono'
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
{H' : SimpleGraph.Subgraph G}
(hle : ∀ (v w : V), SimpleGraph.Subgraph.Adj H v w → SimpleGraph.Subgraph.Adj H' v w)
(hv : H.verts = H'.verts)
(h : SimpleGraph.Subgraph.Connected H)
:
theorem
SimpleGraph.Subgraph.Connected.sup
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
{K : SimpleGraph.Subgraph G}
(hH : SimpleGraph.Subgraph.Connected H)
(hK : SimpleGraph.Subgraph.Connected K)
(hn : Set.Nonempty (H ⊓ K).verts)
:
theorem
SimpleGraph.Walk.toSubgraph_connected
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
theorem
SimpleGraph.Subgraph.induce_union_connected
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
{s : Set V}
{t : Set V}
(sconn : SimpleGraph.Subgraph.Connected (SimpleGraph.Subgraph.induce H s))
(tconn : SimpleGraph.Subgraph.Connected (SimpleGraph.Subgraph.induce H t))
(sintert : Set.Nonempty (s ⊓ t))
:
theorem
SimpleGraph.Subgraph.Connected.adj_union
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
{K : SimpleGraph.Subgraph G}
(Hconn : SimpleGraph.Subgraph.Connected H)
(Kconn : SimpleGraph.Subgraph.Connected K)
{u : V}
{v : V}
(uH : u ∈ H.verts)
(vK : v ∈ K.verts)
(huv : SimpleGraph.Adj G u v)
:
SimpleGraph.Subgraph.Connected (SimpleGraph.Subgraph.induce ⊤ {u, v} ⊔ H ⊔ K)
theorem
SimpleGraph.Subgraph.preconnected_iff_forall_exists_walk_subgraph
{V : Type u}
{G : SimpleGraph V}
(H : SimpleGraph.Subgraph G)
:
SimpleGraph.Subgraph.Preconnected H ↔ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, SimpleGraph.Walk.toSubgraph p ≤ H
theorem
SimpleGraph.Subgraph.connected_iff_forall_exists_walk_subgraph
{V : Type u}
{G : SimpleGraph V}
(H : SimpleGraph.Subgraph G)
:
SimpleGraph.Subgraph.Connected H ↔ Set.Nonempty H.verts ∧ ∀ {u v : V}, u ∈ H.verts → v ∈ H.verts → ∃ p, SimpleGraph.Walk.toSubgraph p ≤ H
theorem
SimpleGraph.induce_union_connected
{V : Type u}
{G : SimpleGraph V}
{s : Set V}
{t : Set V}
(sconn : SimpleGraph.Connected (SimpleGraph.induce s G))
(tconn : SimpleGraph.Connected (SimpleGraph.induce t G))
(sintert : Set.Nonempty (s ∩ t))
:
SimpleGraph.Connected (SimpleGraph.induce (s ∪ t) G)
theorem
SimpleGraph.induce_pair_connected_of_adj
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(huv : SimpleGraph.Adj G u v)
:
SimpleGraph.Connected (SimpleGraph.induce {u, v} G)
theorem
SimpleGraph.Subgraph.Connected.induce_verts
{V : Type u}
{G : SimpleGraph V}
{H : SimpleGraph.Subgraph G}
(h : SimpleGraph.Subgraph.Connected H)
:
SimpleGraph.Connected (SimpleGraph.induce H.verts G)
theorem
SimpleGraph.Walk.connected_induce_support
{V : Type u}
{G : SimpleGraph V}
{u : V}
{v : V}
(p : SimpleGraph.Walk G u v)
:
SimpleGraph.Connected (SimpleGraph.induce {v | v ∈ SimpleGraph.Walk.support p} G)
theorem
SimpleGraph.induce_connected_adj_union
{V : Type u}
{G : SimpleGraph V}
{v : V}
{w : V}
{s : Set V}
{t : Set V}
(sconn : SimpleGraph.Connected (SimpleGraph.induce s G))
(tconn : SimpleGraph.Connected (SimpleGraph.induce t G))
(hv : v ∈ s)
(hw : w ∈ t)
(ha : SimpleGraph.Adj G v w)
:
SimpleGraph.Connected (SimpleGraph.induce (s ∪ t) G)
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' x hu' hv',
SimpleGraph.Reachable (SimpleGraph.induce s' G) { val := u, property := hu' } { val := v, property := hv' })
:
theorem
SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint
{V : Type u}
{G : SimpleGraph V}
{S : Set (Set V)}
(Sn : Set.Nonempty S)
(Snd : ∀ {s t : Set V}, s ∈ S → t ∈ S → Set.Nonempty (s ∩ t))
(Sc : ∀ {s : Set V}, s ∈ S → SimpleGraph.Connected (SimpleGraph.induce s G))
:
theorem
SimpleGraph.extend_finset_to_connected
{V : Type u}
{G : SimpleGraph V}
(Gpc : SimpleGraph.Preconnected G)
{t : Finset V}
(tn : Finset.Nonempty t)
:
∃ t', t ⊆ t' ∧ SimpleGraph.Connected (SimpleGraph.induce (↑t') G)