Documentation

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Connectivity of subgraphs and induced graphs #

Main definitions #

structure SimpleGraph.Subgraph.Preconnected {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) :

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

    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_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 wH'.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 vG.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) :
        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_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) :
        w.toSubgraph.Adj u' v' ∃ (i : ), s(w.getVert i, w.getVert (i + 1)) = s(u', v') i < w.length
        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.vertsv 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.vertsv 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 ss'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 St 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