Documentation

Mathlib.Combinatorics.SimpleGraph.Subgraph

Subgraphs of a simple graph #

A subgraph of a simple graph consists of subsets of the graph's vertices and edges such that the endpoints of each edge are present in the vertex subset. The edge subset is formalized as a sub-relation of the adjacency relation of the simple graph.

Main definitions #

Implementation notes #

Todo #

theorem SimpleGraph.Subgraph.ext {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (y : SimpleGraph.Subgraph G) (verts : x.verts = y.verts) (Adj : x.Adj = y.Adj) :
x = y
theorem SimpleGraph.Subgraph.ext_iff {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (y : SimpleGraph.Subgraph G) :
x = y x.verts = y.verts x.Adj = y.Adj
structure SimpleGraph.Subgraph {V : Type u} (G : SimpleGraph V) :

A subgraph of a SimpleGraph is a subset of vertices along with a restriction of the adjacency relation that is symmetric and is supported by the vertex subset. They also form a bounded lattice.

Thinking of V → V → Prop as Set (V × V), a set of darts (i.e., half-edges), then Subgraph.adj_sub is that the darts of a subgraph are a subset of the darts of G.

Instances For
    @[simp]
    theorem SimpleGraph.singletonSubgraph_Adj {V : Type u} (G : SimpleGraph V) (v : V) :
    ∀ (a a_1 : V), SimpleGraph.Subgraph.Adj (SimpleGraph.singletonSubgraph G v) a a_1 = a a_1
    @[simp]

    The one-vertex subgraph.

    Instances For
      @[simp]
      theorem SimpleGraph.subgraphOfAdj_Adj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) (a : V) (b : V) :
      @[simp]
      theorem SimpleGraph.subgraphOfAdj_verts {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :
      (SimpleGraph.subgraphOfAdj G hvw).verts = {v, w}
      def SimpleGraph.subgraphOfAdj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :

      The one-edge subgraph.

      Instances For
        theorem SimpleGraph.Subgraph.Adj.fst_mem {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : SimpleGraph.Subgraph.Adj H u v) :
        u H.verts
        theorem SimpleGraph.Subgraph.Adj.snd_mem {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : SimpleGraph.Subgraph.Adj H u v) :
        v H.verts
        theorem SimpleGraph.Subgraph.Adj.ne {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : SimpleGraph.Subgraph.Adj H u v) :
        u v
        @[simp]
        theorem SimpleGraph.Subgraph.coe_Adj {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : G'.verts) (w : G'.verts) :

        Coercion from G' : Subgraph G to a SimpleGraph G'.verts.

        Instances For
          @[simp]
          theorem SimpleGraph.Subgraph.coe_adj_sub {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (u : G'.verts) (v : G'.verts) (h : SimpleGraph.Adj (SimpleGraph.Subgraph.coe G') u v) :
          SimpleGraph.Adj G u v
          theorem SimpleGraph.Subgraph.Adj.coe {V : Type u} {G : SimpleGraph V} {H : SimpleGraph.Subgraph G} {u : V} {v : V} (h : SimpleGraph.Subgraph.Adj H u v) :
          SimpleGraph.Adj (SimpleGraph.Subgraph.coe H) { val := u, property := (_ : u H.verts) } { val := v, property := (_ : v H.verts) }

          A subgraph is called a spanning subgraph if it contains all the vertices of G.

          Instances For

            Coercion from Subgraph G to SimpleGraph V. If G' is a spanning subgraph, then G'.spanningCoe yields an isomorphic graph. In general, this adds in all vertices from V as isolated vertices.

            Instances For
              @[simp]
              theorem SimpleGraph.Subgraph.Adj.of_spanningCoe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {u : G'.verts} {v : G'.verts} (h : SimpleGraph.Adj (SimpleGraph.Subgraph.spanningCoe G') u v) :
              SimpleGraph.Adj G u v

              A subgraph is called an induced subgraph if vertices of G' are adjacent if they are adjacent in G.

              Instances For

                H.support is the set of vertices that form edges in the subgraph H.

                Instances For

                  G'.neighborSet v is the set of vertices adjacent to v in G'.

                  Instances For

                    A subgraph as a graph has equivalent neighbor sets.

                    Instances For

                      The edge set of G' consists of a subset of edges of G.

                      Instances For
                        theorem SimpleGraph.Subgraph.mem_verts_if_mem_edge {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {e : Sym2 V} {v : V} (he : e SimpleGraph.Subgraph.edgeSet G') (hv : v e) :
                        v G'.verts

                        The incidenceSet is the set of edges incident to a given vertex.

                        Instances For
                          @[reducible]
                          def SimpleGraph.Subgraph.vert {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (v : V) (h : v G'.verts) :
                          G'.verts

                          Give a vertex as an element of the subgraph's vertex type.

                          Instances For
                            def SimpleGraph.Subgraph.copy {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (V'' : Set V) (hV : V'' = G'.verts) (adj' : VVProp) (hadj : adj' = G'.Adj) :

                            Create an equal copy of a subgraph (see copy_eq) with possibly different definitional equalities. See Note [range copy pattern].

                            Instances For
                              theorem SimpleGraph.Subgraph.copy_eq {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) (V'' : Set V) (hV : V'' = G'.verts) (adj' : VVProp) (hadj : adj' = G'.Adj) :
                              SimpleGraph.Subgraph.copy G' V'' hV adj' hadj = G'

                              The union of two subgraphs.

                              The intersection of two subgraphs.

                              The top subgraph is G as a subgraph of itself.

                              The bot subgraph is the subgraph with no vertices or edges.

                              @[simp]
                              @[simp]
                              @[simp]
                              @[simp]
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_sup {V : Type u} {G : SimpleGraph V} (G₁ : SimpleGraph.Subgraph G) (G₂ : SimpleGraph.Subgraph G) :
                              (G₁ G₂).verts = G₁.verts G₂.verts
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_inf {V : Type u} {G : SimpleGraph V} (G₁ : SimpleGraph.Subgraph G) (G₂ : SimpleGraph.Subgraph G) :
                              (G₁ G₂).verts = G₁.verts G₂.verts
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_top {V : Type u} {G : SimpleGraph V} :
                              .verts = Set.univ
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_bot {V : Type u} {G : SimpleGraph V} :
                              .verts =
                              @[simp]
                              theorem SimpleGraph.Subgraph.sSup_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} :
                              @[simp]
                              theorem SimpleGraph.Subgraph.sInf_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set (SimpleGraph.Subgraph G)} :
                              @[simp]
                              theorem SimpleGraph.Subgraph.iSup_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ιSimpleGraph.Subgraph G} :
                              SimpleGraph.Subgraph.Adj (⨆ (i : ι), f i) a b i, SimpleGraph.Subgraph.Adj (f i) a b
                              @[simp]
                              theorem SimpleGraph.Subgraph.iInf_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ιSimpleGraph.Subgraph G} :
                              SimpleGraph.Subgraph.Adj (⨅ (i : ι), f i) a b (∀ (i : ι), SimpleGraph.Subgraph.Adj (f i) a b) SimpleGraph.Adj G a b
                              theorem SimpleGraph.Subgraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} [Nonempty ι] {f : ιSimpleGraph.Subgraph G} :
                              SimpleGraph.Subgraph.Adj (⨅ (i : ι), f i) a b ∀ (i : ι), SimpleGraph.Subgraph.Adj (f i) a b
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_sSup {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) :
                              (sSup s).verts = ⋃ (G' : SimpleGraph.Subgraph G) (_ : G' s), G'.verts
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_sInf {V : Type u} {G : SimpleGraph V} (s : Set (SimpleGraph.Subgraph G)) :
                              (sInf s).verts = ⋂ (G' : SimpleGraph.Subgraph G) (_ : G' s), G'.verts
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ιSimpleGraph.Subgraph G} :
                              (⨆ (i : ι), f i).verts = ⋃ (i : ι), (f i).verts
                              @[simp]
                              theorem SimpleGraph.Subgraph.verts_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ιSimpleGraph.Subgraph G} :
                              (⨅ (i : ι), f i).verts = ⋂ (i : ι), (f i).verts

                              For subgraphs G₁, G₂, G₁ ≤ G₂ iff G₁.verts ⊆ G₂.verts and ∀ a b, G₁.adj a b → G₂.adj a b.

                              @[simp]
                              theorem SimpleGraph.Subgraph.neighborSet_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιSimpleGraph.Subgraph G) (v : V) :
                              SimpleGraph.Subgraph.neighborSet (⨆ (i : ι), f i) v = ⋃ (i : ι), SimpleGraph.Subgraph.neighborSet (f i) v
                              @[simp]
                              theorem SimpleGraph.Subgraph.neighborSet_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιSimpleGraph.Subgraph G) (v : V) :
                              @[simp]
                              theorem SimpleGraph.Subgraph.edgeSet_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιSimpleGraph.Subgraph G) :
                              SimpleGraph.Subgraph.edgeSet (⨆ (i : ι), f i) = ⋃ (i : ι), SimpleGraph.Subgraph.edgeSet (f i)
                              @[simp]
                              theorem SimpleGraph.Subgraph.edgeSet_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιSimpleGraph.Subgraph G) :
                              @[simp]
                              theorem SimpleGraph.toSubgraph_Adj {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H G) :
                              @[simp]
                              theorem SimpleGraph.toSubgraph_verts {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H G) :
                              (SimpleGraph.toSubgraph H h).verts = Set.univ

                              Turn a subgraph of a SimpleGraph into a member of its subgraph type.

                              Instances For

                                The top of the Subgraph G lattice is equivalent to the graph itself.

                                Instances For

                                  The bottom of the Subgraph G lattice is equivalent to the empty graph on the empty vertex type.

                                  Instances For
                                    @[simp]
                                    theorem SimpleGraph.Subgraph.map_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) :
                                    (SimpleGraph.Subgraph.map f H).verts = f '' H.verts
                                    @[simp]
                                    theorem SimpleGraph.Subgraph.map_Adj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) :
                                    ∀ (a a_1 : W), SimpleGraph.Subgraph.Adj (SimpleGraph.Subgraph.map f H) a a_1 = Relation.Map H.Adj (f) (f) a a_1
                                    def SimpleGraph.Subgraph.map {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G) :

                                    Graph homomorphisms induce a covariant function on subgraphs.

                                    Instances For
                                      @[simp]
                                      theorem SimpleGraph.Subgraph.comap_Adj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G') (u : V) (v : V) :
                                      @[simp]
                                      theorem SimpleGraph.Subgraph.comap_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G') :
                                      (SimpleGraph.Subgraph.comap f H).verts = f ⁻¹' H.verts
                                      def SimpleGraph.Subgraph.comap {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : SimpleGraph.Subgraph G') :

                                      Graph homomorphisms induce a contravariant function on subgraphs.

                                      Instances For
                                        @[simp]
                                        theorem SimpleGraph.Subgraph.inclusion_apply_coe {V : Type u} {G : SimpleGraph V} {x : SimpleGraph.Subgraph G} {y : SimpleGraph.Subgraph G} (h : x y) (v : x.verts) :

                                        Given two subgraphs, one a subgraph of the other, there is an induced injective homomorphism of the subgraphs as graphs.

                                        Instances For
                                          @[simp]
                                          theorem SimpleGraph.Subgraph.hom_apply {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) (v : x.verts) :

                                          There is an induced injective homomorphism of a subgraph of G into G.

                                          Instances For
                                            @[simp]
                                            theorem SimpleGraph.Subgraph.coe_hom {V : Type u} {G : SimpleGraph V} (x : SimpleGraph.Subgraph G) :
                                            ↑(SimpleGraph.Subgraph.hom x) = fun v => v

                                            There is an induced injective homomorphism of a subgraph of G as a spanning subgraph into G.

                                            Instances For
                                              instance SimpleGraph.Subgraph.finiteAt {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (v : G'.verts) [DecidableRel G'.Adj] [Fintype ↑(SimpleGraph.neighborSet G v)] :

                                              If a graph is locally finite at a vertex, then so is a subgraph of that graph.

                                              If a subgraph is locally finite at a vertex, then so are subgraphs of that subgraph.

                                              This is not an instance because G'' cannot be inferred.

                                              Instances For

                                                The degree of a vertex in a subgraph. It's zero for vertices outside the subgraph.

                                                Instances For

                                                  Properties of singletonSubgraph and subgraphOfAdj #

                                                  instance SimpleGraph.nonempty_subgraphOfAdj_verts {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :
                                                  @[simp]
                                                  theorem SimpleGraph.map_subgraphOfAdj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :
                                                  @[simp]
                                                  theorem SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) (hv : u v) (hw : u w) :
                                                  theorem SimpleGraph.neighborSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (hvw : SimpleGraph.Adj G v w) :
                                                  SimpleGraph.Subgraph.neighborSet (SimpleGraph.subgraphOfAdj G hvw) u = (if u = v then {w} else ) if u = w then {v} else

                                                  Subgraphs of subgraphs #

                                                  @[reducible]

                                                  Given a subgraph of a subgraph of G, construct a subgraph of G.

                                                  Instances For
                                                    @[reducible]

                                                    Given a subgraph of G, restrict it to being a subgraph of another subgraph G' by taking the portion of G that intersects G'.

                                                    Instances For
                                                      theorem SimpleGraph.Subgraph.coeSubgraph_Adj {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} (G'' : SimpleGraph.Subgraph (SimpleGraph.Subgraph.coe G')) (v : V) (w : V) :
                                                      SimpleGraph.Subgraph.Adj (SimpleGraph.Subgraph.coeSubgraph G'') v w hv hw, SimpleGraph.Subgraph.Adj G'' { val := v, property := hv } { val := w, property := hw }
                                                      theorem SimpleGraph.Subgraph.coeSubgraph_injective {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph.Subgraph G) :
                                                      Function.Injective SimpleGraph.Subgraph.coeSubgraph

                                                      Edge deletion #

                                                      Given a subgraph G' and a set of vertex pairs, remove all of the corresponding edges from its edge set, if present.

                                                      See also: SimpleGraph.deleteEdges.

                                                      Instances For
                                                        @[simp]

                                                        Induced subgraphs #

                                                        @[simp]

                                                        The induced subgraph of a subgraph. The expectation is that s ⊆ G'.verts for the usual notion of an induced subgraph, but, in general, s is taken to be the new vertex set and edges are induced from the subgraph G'.

                                                        Instances For
                                                          theorem SimpleGraph.Subgraph.induce_mono {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph.Subgraph G} {G'' : SimpleGraph.Subgraph G} {s : Set V} {s' : Set V} (hg : G' G'') (hs : s s') :
                                                          @[reducible]

                                                          Given a subgraph and a set of vertices, delete all the vertices from the subgraph, if present. Any edges incident to the deleted vertices are deleted as well.

                                                          Instances For