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 : SimpleGraph.Subgraph G) : 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 : SimpleGraph.Preconnected (SimpleGraph.Subgraph.coe H)

instance SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : Coe (SimpleGraph.Subgraph.Preconnected H) (SimpleGraph.Preconnected (SimpleGraph.Subgraph.coe H))

Equations

• SimpleGraph.Subgraph.instCoePreconnectedPreconnectedElemVertsCoe = { coe := ⋯ }

instance SimpleGraph.Subgraph.instCoeFunPreconnectedForAllElemVertsReachableCoe {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : CoeFun (SimpleGraph.Subgraph.Preconnected H) fun (x : SimpleGraph.Subgraph.Preconnected H) => ∀ (u v : ↑H.verts), SimpleGraph.Reachable (SimpleGraph.Subgraph.coe H) u v

Equations

• SimpleGraph.Subgraph.instCoeFunPreconnectedForAllElemVertsReachableCoe = { coe := ⋯ }

theorem SimpleGraph.Subgraph.preconnected_iff {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.Preconnected H ↔ SimpleGraph.Preconnected (SimpleGraph.Subgraph.coe H)

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

instance SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : Coe (SimpleGraph.Subgraph.Connected H) (SimpleGraph.Connected (SimpleGraph.Subgraph.coe H))

Equations

• SimpleGraph.Subgraph.instCoeConnectedConnectedElemVertsCoe = { coe := ⋯ }

instance SimpleGraph.Subgraph.instCoeFunConnectedForAllElemVertsReachableCoe {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : CoeFun (SimpleGraph.Subgraph.Connected H) fun (x : SimpleGraph.Subgraph.Connected H) => ∀ (u v : ↑H.verts), SimpleGraph.Reachable (SimpleGraph.Subgraph.coe H) u v

Equations

• SimpleGraph.Subgraph.instCoeFunConnectedForAllElemVertsReachableCoe = { coe := ⋯ }

theorem SimpleGraph.Subgraph.connected_iff' {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.Connected H ↔ SimpleGraph.Connected (SimpleGraph.Subgraph.coe H)

theorem SimpleGraph.Subgraph.connected_iff {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} : SimpleGraph.Subgraph.Connected H ↔ SimpleGraph.Subgraph.Preconnected H ∧ Set.Nonempty H.verts

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

theorem SimpleGraph.Subgraph.singletonSubgraph_connected {V : Type u} {G : SimpleGraph V} {v : V} : SimpleGraph.Subgraph.Connected (SimpleGraph.singletonSubgraph G v)

@[simp]

theorem SimpleGraph.Subgraph.subgraphOfAdj_connected {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) : SimpleGraph.Subgraph.Connected (SimpleGraph.subgraphOfAdj G hvw)

theorem SimpleGraph.Subgraph.top_induce_pair_connected_of_adj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (huv : G.Adj u v) : SimpleGraph.Subgraph.Connected (SimpleGraph.Subgraph.induce ⊤ {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) : 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), H.Adj v w → H'.Adj v w) (hv : H.verts = H'.verts) (h : SimpleGraph.Subgraph.Connected 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) : SimpleGraph.Subgraph.Connected (H ⊔ K)

theorem SimpleGraph.Walk.toSubgraph_connected {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) : SimpleGraph.Subgraph.Connected (SimpleGraph.Walk.toSubgraph p)

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)) : SimpleGraph.Subgraph.Connected (SimpleGraph.Subgraph.induce H (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 : G.Adj 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 G u v), 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 G u v), SimpleGraph.Walk.toSubgraph p ≤ H

theorem SimpleGraph.connected_induce_iff {V : Type u} {G : SimpleGraph V} {s : Set V} : SimpleGraph.Connected (SimpleGraph.induce s G) ↔ SimpleGraph.Subgraph.Connected (SimpleGraph.Subgraph.induce ⊤ s)

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 : G.Adj 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_1 : V | v_1 ∈ 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 : G.Adj 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' ⊆ s, ∃ (hu' : u ∈ s') (hv' : v ∈ s'), SimpleGraph.Reachable (SimpleGraph.induce s' G) { val := u, property := hu' } { val := v, property := hv' }) : SimpleGraph.Connected (SimpleGraph.induce s G)

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)) : 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 : t.Nonempty) : ∃ (t' : Finset V), t ⊆ t' ∧ SimpleGraph.Connected (SimpleGraph.induce (↑t') G)