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 : G.Subgraph) (y : G.Subgraph) (verts : x.verts = y.verts) (Adj : x.Adj = y.Adj) :
x = y
theorem SimpleGraph.Subgraph.ext_iff {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) (y : G.Subgraph) :
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.

  • verts : Set V
  • Adj : VVProp
  • adj_sub : ∀ {v w : V}, self.Adj v wG.Adj v w
  • edge_vert : ∀ {v w : V}, self.Adj v wv self.verts
  • symm : Symmetric self.Adj
Instances For
    theorem SimpleGraph.Subgraph.adj_sub {V : Type u} {G : SimpleGraph V} (self : G.Subgraph) {v : V} {w : V} :
    self.Adj v wG.Adj v w
    theorem SimpleGraph.Subgraph.edge_vert {V : Type u} {G : SimpleGraph V} (self : G.Subgraph) {v : V} {w : V} :
    self.Adj v wv self.verts
    theorem SimpleGraph.Subgraph.symm {V : Type u} {G : SimpleGraph V} (self : G.Subgraph) :
    Symmetric self.Adj
    @[simp]
    theorem SimpleGraph.singletonSubgraph_adj {V : Type u} (G : SimpleGraph V) (v : V) :
    ∀ (a a_1 : V), (G.singletonSubgraph v).Adj a a_1 = a a_1
    @[simp]
    theorem SimpleGraph.singletonSubgraph_verts {V : Type u} (G : SimpleGraph V) (v : V) :
    (G.singletonSubgraph v).verts = {v}
    def SimpleGraph.singletonSubgraph {V : Type u} (G : SimpleGraph V) (v : V) :
    G.Subgraph

    The one-vertex subgraph.

    Equations
    • G.singletonSubgraph v = { verts := {v}, Adj := , adj_sub := , edge_vert := , symm := }
    Instances For
      @[simp]
      theorem SimpleGraph.subgraphOfAdj_verts {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : G.Adj v w) :
      (G.subgraphOfAdj hvw).verts = {v, w}
      @[simp]
      theorem SimpleGraph.subgraphOfAdj_adj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : G.Adj v w) (a : V) (b : V) :
      (G.subgraphOfAdj hvw).Adj a b = (s(v, w) = s(a, b))
      def SimpleGraph.subgraphOfAdj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} (hvw : G.Adj v w) :
      G.Subgraph

      The one-edge subgraph.

      Equations
      • G.subgraphOfAdj hvw = { verts := {v, w}, Adj := fun (a b : V) => s(v, w) = s(a, b), adj_sub := , edge_vert := , symm := }
      Instances For
        theorem SimpleGraph.Subgraph.loopless {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :
        theorem SimpleGraph.Subgraph.adj_comm {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) (w : V) :
        G'.Adj v w G'.Adj w v
        theorem SimpleGraph.Subgraph.adj_symm {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) {u : V} {v : V} (h : G'.Adj u v) :
        G'.Adj v u
        theorem SimpleGraph.Subgraph.Adj.symm {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {u : V} {v : V} (h : G'.Adj u v) :
        G'.Adj v u
        theorem SimpleGraph.Subgraph.Adj.adj_sub {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
        G.Adj u v
        theorem SimpleGraph.Subgraph.Adj.fst_mem {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
        u H.verts
        theorem SimpleGraph.Subgraph.Adj.snd_mem {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
        v H.verts
        theorem SimpleGraph.Subgraph.Adj.ne {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
        u v
        @[simp]
        theorem SimpleGraph.Subgraph.coe_adj {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : G'.verts) (w : G'.verts) :
        G'.coe.Adj v w = G'.Adj v w
        def SimpleGraph.Subgraph.coe {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :
        SimpleGraph G'.verts

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

        Equations
        • G'.coe = { Adj := fun (v w : G'.verts) => G'.Adj v w, symm := , loopless := }
        Instances For
          @[simp]
          theorem SimpleGraph.Subgraph.coe_adj_sub {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (u : G'.verts) (v : G'.verts) (h : G'.coe.Adj u v) :
          G.Adj u v
          theorem SimpleGraph.Subgraph.Adj.coe {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u : V} {v : V} (h : H.Adj u v) :
          H.coe.Adj u, v,
          def SimpleGraph.Subgraph.IsSpanning {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :

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

          Equations
          • G'.IsSpanning = ∀ (v : V), v G'.verts
          Instances For
            theorem SimpleGraph.Subgraph.isSpanning_iff {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
            G'.IsSpanning G'.verts = Set.univ
            @[simp]
            theorem SimpleGraph.Subgraph.spanningCoe_adj {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :
            ∀ (a a_1 : V), G'.spanningCoe.Adj a a_1 = G'.Adj a a_1
            def SimpleGraph.Subgraph.spanningCoe {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :

            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.

            Equations
            • G'.spanningCoe = { Adj := G'.Adj, symm := , loopless := }
            Instances For
              @[simp]
              theorem SimpleGraph.Subgraph.Adj.of_spanningCoe {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {u : G'.verts} {v : G'.verts} (h : G'.spanningCoe.Adj u v) :
              G.Adj u v
              theorem SimpleGraph.Subgraph.spanningCoe_inj {V : Type u} {G : SimpleGraph V} {G₁ : G.Subgraph} {G₂ : G.Subgraph} :
              G₁.spanningCoe = G₂.spanningCoe G₁.Adj = G₂.Adj
              @[simp]
              theorem SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_apply_coe {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (h : G'.IsSpanning) (v : V) :
              ((G'.spanningCoeEquivCoeOfSpanning h) v) = v
              @[simp]
              theorem SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning_symm_apply {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (h : G'.IsSpanning) (v : G'.verts) :
              (RelIso.symm (G'.spanningCoeEquivCoeOfSpanning h)) v = v
              def SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (h : G'.IsSpanning) :
              G'.spanningCoe ≃g G'.coe

              spanningCoe is equivalent to coe for a subgraph that IsSpanning.

              Equations
              • G'.spanningCoeEquivCoeOfSpanning h = { toFun := fun (v : V) => v, , invFun := fun (v : G'.verts) => v, left_inv := , right_inv := , map_rel_iff' := }
              Instances For
                def SimpleGraph.Subgraph.IsInduced {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :

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

                Equations
                • G'.IsInduced = ∀ {v w : V}, v G'.vertsw G'.vertsG.Adj v wG'.Adj v w
                Instances For
                  def SimpleGraph.Subgraph.support {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) :
                  Set V

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

                  Equations
                  Instances For
                    theorem SimpleGraph.Subgraph.mem_support {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) {v : V} :
                    v H.support ∃ (w : V), H.Adj v w
                    theorem SimpleGraph.Subgraph.support_subset_verts {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) :
                    H.support H.verts
                    def SimpleGraph.Subgraph.neighborSet {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) :
                    Set V

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

                    Equations
                    • G'.neighborSet v = {w : V | G'.Adj v w}
                    Instances For
                      theorem SimpleGraph.Subgraph.neighborSet_subset {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) :
                      G'.neighborSet v G.neighborSet v
                      theorem SimpleGraph.Subgraph.neighborSet_subset_verts {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) :
                      G'.neighborSet v G'.verts
                      @[simp]
                      theorem SimpleGraph.Subgraph.mem_neighborSet {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) (w : V) :
                      w G'.neighborSet v G'.Adj v w
                      def SimpleGraph.Subgraph.coeNeighborSetEquiv {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (v : G'.verts) :
                      (G'.coe.neighborSet v) (G'.neighborSet v)

                      A subgraph as a graph has equivalent neighbor sets.

                      Equations
                      • SimpleGraph.Subgraph.coeNeighborSetEquiv v = { toFun := fun (w : (G'.coe.neighborSet v)) => w, , invFun := fun (w : (G'.neighborSet v)) => w, , , left_inv := , right_inv := }
                      Instances For
                        def SimpleGraph.Subgraph.edgeSet {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :
                        Set (Sym2 V)

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

                        Equations
                        Instances For
                          theorem SimpleGraph.Subgraph.edgeSet_subset {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :
                          G'.edgeSet G.edgeSet
                          @[simp]
                          theorem SimpleGraph.Subgraph.mem_edgeSet {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} {w : V} :
                          s(v, w) G'.edgeSet G'.Adj v w
                          theorem SimpleGraph.Subgraph.mem_verts_if_mem_edge {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {e : Sym2 V} {v : V} (he : e G'.edgeSet) (hv : v e) :
                          v G'.verts
                          def SimpleGraph.Subgraph.incidenceSet {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) :
                          Set (Sym2 V)

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

                          Equations
                          Instances For
                            theorem SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) :
                            G'.incidenceSet v G.incidenceSet v
                            theorem SimpleGraph.Subgraph.incidenceSet_subset {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) :
                            G'.incidenceSet v G'.edgeSet
                            @[reducible, inline]
                            abbrev SimpleGraph.Subgraph.vert {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) (h : v G'.verts) :
                            G'.verts

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

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

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

                              Equations
                              • G'.copy V'' hV adj' hadj = { verts := V'', Adj := adj', adj_sub := , edge_vert := , symm := }
                              Instances For
                                theorem SimpleGraph.Subgraph.copy_eq {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (V'' : Set V) (hV : V'' = G'.verts) (adj' : VVProp) (hadj : adj' = G'.Adj) :
                                G'.copy V'' hV adj' hadj = G'
                                instance SimpleGraph.Subgraph.instSup {V : Type u} {G : SimpleGraph V} :
                                Sup G.Subgraph

                                The union of two subgraphs.

                                Equations
                                • SimpleGraph.Subgraph.instSup = { sup := fun (G₁ G₂ : G.Subgraph) => { verts := G₁.verts G₂.verts, Adj := G₁.Adj G₂.Adj, adj_sub := , edge_vert := , symm := } }
                                instance SimpleGraph.Subgraph.instInf {V : Type u} {G : SimpleGraph V} :
                                Inf G.Subgraph

                                The intersection of two subgraphs.

                                Equations
                                • SimpleGraph.Subgraph.instInf = { inf := fun (G₁ G₂ : G.Subgraph) => { verts := G₁.verts G₂.verts, Adj := G₁.Adj G₂.Adj, adj_sub := , edge_vert := , symm := } }
                                instance SimpleGraph.Subgraph.instTop {V : Type u} {G : SimpleGraph V} :
                                Top G.Subgraph

                                The top subgraph is G as a subgraph of itself.

                                Equations
                                • SimpleGraph.Subgraph.instTop = { top := { verts := Set.univ, Adj := G.Adj, adj_sub := , edge_vert := , symm := } }
                                instance SimpleGraph.Subgraph.instBot {V : Type u} {G : SimpleGraph V} :
                                Bot G.Subgraph

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

                                Equations
                                • SimpleGraph.Subgraph.instBot = { bot := { verts := , Adj := , adj_sub := , edge_vert := , symm := } }
                                instance SimpleGraph.Subgraph.instSupSet {V : Type u} {G : SimpleGraph V} :
                                SupSet G.Subgraph
                                Equations
                                • One or more equations did not get rendered due to their size.
                                instance SimpleGraph.Subgraph.instInfSet {V : Type u} {G : SimpleGraph V} :
                                InfSet G.Subgraph
                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[simp]
                                theorem SimpleGraph.Subgraph.sup_adj {V : Type u} {G : SimpleGraph V} {G₁ : G.Subgraph} {G₂ : G.Subgraph} {a : V} {b : V} :
                                (G₁ G₂).Adj a b G₁.Adj a b G₂.Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.inf_adj {V : Type u} {G : SimpleGraph V} {G₁ : G.Subgraph} {G₂ : G.Subgraph} {a : V} {b : V} :
                                (G₁ G₂).Adj a b G₁.Adj a b G₂.Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.top_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} :
                                .Adj a b G.Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.not_bot_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} :
                                ¬.Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.verts_sup {V : Type u} {G : SimpleGraph V} (G₁ : G.Subgraph) (G₂ : G.Subgraph) :
                                (G₁ G₂).verts = G₁.verts G₂.verts
                                @[simp]
                                theorem SimpleGraph.Subgraph.verts_inf {V : Type u} {G : SimpleGraph V} (G₁ : G.Subgraph) (G₂ : G.Subgraph) :
                                (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 G.Subgraph} :
                                (sSup s).Adj a b G_1s, G_1.Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.sInf_adj {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set G.Subgraph} :
                                (sInf s).Adj a b (G's, G'.Adj a b) G.Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.iSup_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ιG.Subgraph} :
                                (⨆ (i : ι), f i).Adj a b ∃ (i : ι), (f i).Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.iInf_adj {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {f : ιG.Subgraph} :
                                (⨅ (i : ι), f i).Adj a b (∀ (i : ι), (f i).Adj a b) G.Adj a b
                                theorem SimpleGraph.Subgraph.sInf_adj_of_nonempty {V : Type u} {G : SimpleGraph V} {a : V} {b : V} {s : Set G.Subgraph} (hs : s.Nonempty) :
                                (sInf s).Adj a b G's, G'.Adj a b
                                theorem SimpleGraph.Subgraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {a : V} {b : V} [Nonempty ι] {f : ιG.Subgraph} :
                                (⨅ (i : ι), f i).Adj a b ∀ (i : ι), (f i).Adj a b
                                @[simp]
                                theorem SimpleGraph.Subgraph.verts_sSup {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) :
                                (sSup s).verts = G's, G'.verts
                                @[simp]
                                theorem SimpleGraph.Subgraph.verts_sInf {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) :
                                (sInf s).verts = G's, G'.verts
                                @[simp]
                                theorem SimpleGraph.Subgraph.verts_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ιG.Subgraph} :
                                (⨆ (i : ι), f i).verts = ⋃ (i : ι), (f i).verts
                                @[simp]
                                theorem SimpleGraph.Subgraph.verts_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} {f : ιG.Subgraph} :
                                (⨅ (i : ι), f i).verts = ⋂ (i : ι), (f i).verts
                                theorem SimpleGraph.Subgraph.verts_spanningCoe_injective {V : Type u} {G : SimpleGraph V} :
                                Function.Injective fun (G' : G.Subgraph) => (G'.verts, G'.spanningCoe)

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

                                Equations
                                Equations
                                • SimpleGraph.Subgraph.instBoundedOrder = BoundedOrder.mk
                                Equations
                                Equations
                                • SimpleGraph.Subgraph.subgraphInhabited = { default := }
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_sup {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {H' : G.Subgraph} (v : V) :
                                (H H').neighborSet v = H.neighborSet v H'.neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_inf {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {H' : G.Subgraph} (v : V) :
                                (H H').neighborSet v = H.neighborSet v H'.neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_top {V : Type u} {G : SimpleGraph V} (v : V) :
                                .neighborSet v = G.neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_bot {V : Type u} {G : SimpleGraph V} (v : V) :
                                .neighborSet v =
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_sSup {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) (v : V) :
                                (sSup s).neighborSet v = G's, G'.neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_sInf {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) (v : V) :
                                (sInf s).neighborSet v = (G's, G'.neighborSet v) G.neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιG.Subgraph) (v : V) :
                                (⨆ (i : ι), f i).neighborSet v = ⋃ (i : ι), (f i).neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.neighborSet_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιG.Subgraph) (v : V) :
                                (⨅ (i : ι), f i).neighborSet v = (⋂ (i : ι), (f i).neighborSet v) G.neighborSet v
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_top {V : Type u} {G : SimpleGraph V} :
                                .edgeSet = G.edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_bot {V : Type u} {G : SimpleGraph V} :
                                .edgeSet =
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_inf {V : Type u} {G : SimpleGraph V} {H₁ : G.Subgraph} {H₂ : G.Subgraph} :
                                (H₁ H₂).edgeSet = H₁.edgeSet H₂.edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_sup {V : Type u} {G : SimpleGraph V} {H₁ : G.Subgraph} {H₂ : G.Subgraph} :
                                (H₁ H₂).edgeSet = H₁.edgeSet H₂.edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_sSup {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) :
                                (sSup s).edgeSet = G's, G'.edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_sInf {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) :
                                (sInf s).edgeSet = (G's, G'.edgeSet) G.edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_iSup {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιG.Subgraph) :
                                (⨆ (i : ι), f i).edgeSet = ⋃ (i : ι), (f i).edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.edgeSet_iInf {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ιG.Subgraph) :
                                (⨅ (i : ι), f i).edgeSet = (⋂ (i : ι), (f i).edgeSet) G.edgeSet
                                @[simp]
                                theorem SimpleGraph.Subgraph.spanningCoe_top {V : Type u} {G : SimpleGraph V} :
                                .spanningCoe = G
                                @[simp]
                                theorem SimpleGraph.Subgraph.spanningCoe_bot {V : Type u} {G : SimpleGraph V} :
                                .spanningCoe =
                                @[simp]
                                theorem SimpleGraph.toSubgraph_adj {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H G) :
                                ∀ (a a_1 : V), (SimpleGraph.toSubgraph H h).Adj a a_1 = H.Adj a a_1
                                @[simp]
                                theorem SimpleGraph.toSubgraph_verts {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H G) :
                                (SimpleGraph.toSubgraph H h).verts = Set.univ
                                def SimpleGraph.toSubgraph {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H G) :
                                G.Subgraph

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

                                Equations
                                Instances For
                                  theorem SimpleGraph.Subgraph.support_mono {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {H' : G.Subgraph} (h : H H') :
                                  H.support H'.support
                                  theorem SimpleGraph.toSubgraph.isSpanning {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H G) :
                                  (SimpleGraph.toSubgraph H h).IsSpanning
                                  theorem SimpleGraph.Subgraph.spanningCoe_le_of_le {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {H' : G.Subgraph} (h : H H') :
                                  H.spanningCoe H'.spanningCoe

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

                                  Equations
                                  • SimpleGraph.Subgraph.topEquiv = { toFun := fun (v : .verts) => v, invFun := fun (v : V) => v, trivial, left_inv := , right_inv := , map_rel_iff' := }
                                  Instances For

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

                                    Equations
                                    • SimpleGraph.Subgraph.botEquiv = { toFun := fun (v : .verts) => False.elim , invFun := fun (v : Empty) => v.elim, left_inv := , right_inv := , map_rel_iff' := }
                                    Instances For
                                      theorem SimpleGraph.Subgraph.edgeSet_mono {V : Type u} {G : SimpleGraph V} {H₁ : G.Subgraph} {H₂ : G.Subgraph} (h : H₁ H₂) :
                                      H₁.edgeSet H₂.edgeSet
                                      theorem Disjoint.edgeSet {V : Type u} {G : SimpleGraph V} {H₁ : G.Subgraph} {H₂ : G.Subgraph} (h : Disjoint H₁ H₂) :
                                      Disjoint H₁.edgeSet H₂.edgeSet
                                      @[simp]
                                      theorem SimpleGraph.Subgraph.map_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph) :
                                      (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 : G.Subgraph) :
                                      ∀ (a a_1 : W), (SimpleGraph.Subgraph.map f H).Adj 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 : G.Subgraph) :
                                      G'.Subgraph

                                      Graph homomorphisms induce a covariant function on subgraphs.

                                      Equations
                                      Instances For
                                        theorem SimpleGraph.Subgraph.map_sup {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {H : G.Subgraph} {H' : G.Subgraph} :
                                        @[simp]
                                        theorem SimpleGraph.Subgraph.comap_adj {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G'.Subgraph) (u : V) (v : V) :
                                        (SimpleGraph.Subgraph.comap f H).Adj u v = (G.Adj u v H.Adj (f u) (f v))
                                        @[simp]
                                        theorem SimpleGraph.Subgraph.comap_verts {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G'.Subgraph) :
                                        (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 : G'.Subgraph) :
                                        G.Subgraph

                                        Graph homomorphisms induce a contravariant function on subgraphs.

                                        Equations
                                        Instances For
                                          theorem SimpleGraph.Subgraph.map_le_iff_le_comap {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph) (H' : G'.Subgraph) :
                                          @[simp]
                                          theorem SimpleGraph.Subgraph.inclusion_apply_coe {V : Type u} {G : SimpleGraph V} {x : G.Subgraph} {y : G.Subgraph} (h : x y) (v : x.verts) :
                                          def SimpleGraph.Subgraph.inclusion {V : Type u} {G : SimpleGraph V} {x : G.Subgraph} {y : G.Subgraph} (h : x y) :
                                          x.coe →g y.coe

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

                                          Equations
                                          Instances For
                                            theorem SimpleGraph.Subgraph.inclusion.injective {V : Type u} {G : SimpleGraph V} {x : G.Subgraph} {y : G.Subgraph} (h : x y) :
                                            @[simp]
                                            theorem SimpleGraph.Subgraph.hom_apply {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) (v : x.verts) :
                                            x.hom v = v
                                            def SimpleGraph.Subgraph.hom {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) :
                                            x.coe →g G

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

                                            Equations
                                            • x.hom = { toFun := fun (v : x.verts) => v, map_rel' := }
                                            Instances For
                                              @[simp]
                                              theorem SimpleGraph.Subgraph.coe_hom {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) :
                                              x.hom = fun (v : x.verts) => v
                                              theorem SimpleGraph.Subgraph.hom.injective {V : Type u} {G : SimpleGraph V} {x : G.Subgraph} :
                                              @[simp]
                                              theorem SimpleGraph.Subgraph.spanningHom_apply {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) (a : V) :
                                              x.spanningHom a = id a
                                              def SimpleGraph.Subgraph.spanningHom {V : Type u} {G : SimpleGraph V} (x : G.Subgraph) :
                                              x.spanningCoe →g G

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

                                              Equations
                                              • x.spanningHom = { toFun := id, map_rel' := }
                                              Instances For
                                                theorem SimpleGraph.Subgraph.spanningHom.injective {V : Type u} {G : SimpleGraph V} {x : G.Subgraph} :
                                                Function.Injective x.spanningHom
                                                theorem SimpleGraph.Subgraph.neighborSet_subset_of_subgraph {V : Type u} {G : SimpleGraph V} {x : G.Subgraph} {y : G.Subgraph} (h : x y) (v : V) :
                                                x.neighborSet v y.neighborSet v
                                                instance SimpleGraph.Subgraph.neighborSet.decidablePred {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) [h : DecidableRel G'.Adj] (v : V) :
                                                DecidablePred fun (x : V) => x G'.neighborSet v
                                                Equations
                                                instance SimpleGraph.Subgraph.finiteAt {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (v : G'.verts) [DecidableRel G'.Adj] [Fintype (G.neighborSet v)] :
                                                Fintype (G'.neighborSet v)

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

                                                Equations
                                                def SimpleGraph.Subgraph.finiteAtOfSubgraph {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G.Subgraph} [DecidableRel G'.Adj] (h : G' G'') (v : G'.verts) [Fintype (G''.neighborSet v)] :
                                                Fintype (G'.neighborSet v)

                                                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.

                                                Equations
                                                Instances For
                                                  instance SimpleGraph.Subgraph.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) [Fintype G'.verts] (v : V) [DecidablePred fun (x : V) => x G'.neighborSet v] :
                                                  Fintype (G'.neighborSet v)
                                                  Equations
                                                  • G'.instFintypeElemNeighborSetOfVertsOfDecidablePredMemSet v = G'.verts.fintypeSubset
                                                  instance SimpleGraph.Subgraph.coeFiniteAt {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (v : G'.verts) [Fintype (G'.neighborSet v)] :
                                                  Fintype (G'.coe.neighborSet v)
                                                  Equations
                                                  theorem SimpleGraph.Subgraph.IsSpanning.card_verts {V : Type u} {G : SimpleGraph V} [Fintype V] {G' : G.Subgraph} [Fintype G'.verts] (h : G'.IsSpanning) :
                                                  G'.verts.toFinset.card = Fintype.card V
                                                  def SimpleGraph.Subgraph.degree {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) [Fintype (G'.neighborSet v)] :

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

                                                  Equations
                                                  Instances For
                                                    theorem SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [Fintype (G'.neighborSet v)] :
                                                    (G'.neighborSet v).toFinset.card = G'.degree v
                                                    theorem SimpleGraph.Subgraph.degree_le {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V) [Fintype (G'.neighborSet v)] [Fintype (G.neighborSet v)] :
                                                    G'.degree v G.degree v
                                                    theorem SimpleGraph.Subgraph.degree_le' {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (G'' : G.Subgraph) (h : G' G'') (v : V) [Fintype (G'.neighborSet v)] [Fintype (G''.neighborSet v)] :
                                                    G'.degree v G''.degree v
                                                    @[simp]
                                                    theorem SimpleGraph.Subgraph.coe_degree {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : G'.verts) [Fintype (G'.coe.neighborSet v)] [Fintype (G'.neighborSet v)] :
                                                    G'.coe.degree v = G'.degree v
                                                    @[simp]
                                                    theorem SimpleGraph.Subgraph.degree_spanningCoe {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (v : V) [Fintype (G'.neighborSet v)] [Fintype (G'.spanningCoe.neighborSet v)] :
                                                    G'.spanningCoe.degree v = G'.degree v
                                                    theorem SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [Fintype (G'.neighborSet v)] :
                                                    G'.degree v = 1 ∃! w : V, G'.Adj v w

                                                    Properties of singletonSubgraph and subgraphOfAdj #

                                                    instance SimpleGraph.nonempty_singletonSubgraph_verts {V : Type u} {G : SimpleGraph V} (v : V) :
                                                    Nonempty (G.singletonSubgraph v).verts
                                                    Equations
                                                    • =
                                                    @[simp]
                                                    theorem SimpleGraph.singletonSubgraph_le_iff {V : Type u} {G : SimpleGraph V} (v : V) (H : G.Subgraph) :
                                                    G.singletonSubgraph v H v H.verts
                                                    @[simp]
                                                    theorem SimpleGraph.map_singletonSubgraph {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {v : V} :
                                                    SimpleGraph.Subgraph.map f (G.singletonSubgraph v) = G'.singletonSubgraph (f v)
                                                    @[simp]
                                                    theorem SimpleGraph.neighborSet_singletonSubgraph {V : Type u} {G : SimpleGraph V} (v : V) (w : V) :
                                                    (G.singletonSubgraph v).neighborSet w =
                                                    @[simp]
                                                    theorem SimpleGraph.edgeSet_singletonSubgraph {V : Type u} {G : SimpleGraph V} (v : V) :
                                                    (G.singletonSubgraph v).edgeSet =
                                                    theorem SimpleGraph.eq_singletonSubgraph_iff_verts_eq {V : Type u} {G : SimpleGraph V} (H : G.Subgraph) {v : V} :
                                                    H = G.singletonSubgraph v H.verts = {v}
                                                    instance SimpleGraph.nonempty_subgraphOfAdj_verts {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    Nonempty (G.subgraphOfAdj hvw).verts
                                                    Equations
                                                    • =
                                                    @[simp]
                                                    theorem SimpleGraph.edgeSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    (G.subgraphOfAdj hvw).edgeSet = {s(v, w)}
                                                    theorem SimpleGraph.subgraphOfAdj_le_of_adj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (H : G.Subgraph) (h : H.Adj v w) :
                                                    G.subgraphOfAdj H
                                                    theorem SimpleGraph.subgraphOfAdj_symm {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    G.subgraphOfAdj = G.subgraphOfAdj hvw
                                                    @[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 : G.Adj v w) :
                                                    SimpleGraph.Subgraph.map f (G.subgraphOfAdj hvw) = G'.subgraphOfAdj
                                                    theorem SimpleGraph.neighborSet_subgraphOfAdj_subset {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    (G.subgraphOfAdj hvw).neighborSet u {v, w}
                                                    @[simp]
                                                    theorem SimpleGraph.neighborSet_fst_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    (G.subgraphOfAdj hvw).neighborSet v = {w}
                                                    @[simp]
                                                    theorem SimpleGraph.neighborSet_snd_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    (G.subgraphOfAdj hvw).neighborSet w = {v}
                                                    @[simp]
                                                    theorem SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (hvw : G.Adj v w) (hv : u v) (hw : u w) :
                                                    (G.subgraphOfAdj hvw).neighborSet u =
                                                    theorem SimpleGraph.neighborSet_subgraphOfAdj {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                    (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ) if u = w then {v} else
                                                    theorem SimpleGraph.singletonSubgraph_fst_le_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {h : G.Adj u v} :
                                                    G.singletonSubgraph u G.subgraphOfAdj h
                                                    theorem SimpleGraph.singletonSubgraph_snd_le_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {h : G.Adj u v} :
                                                    G.singletonSubgraph v G.subgraphOfAdj h

                                                    Subgraphs of subgraphs #

                                                    @[reducible, inline]
                                                    abbrev SimpleGraph.Subgraph.coeSubgraph {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                    G'.coe.SubgraphG.Subgraph

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

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      abbrev SimpleGraph.Subgraph.restrict {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                      G.SubgraphG'.coe.Subgraph

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

                                                      Equations
                                                      Instances For
                                                        theorem SimpleGraph.Subgraph.coeSubgraph_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph) (v : V) (w : V) :
                                                        (SimpleGraph.Subgraph.coeSubgraph G'').Adj v w ∃ (hv : v G'.verts) (hw : w G'.verts), G''.Adj v, hv w, hw
                                                        theorem SimpleGraph.Subgraph.restrict_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G.Subgraph} (v : G'.verts) (w : G'.verts) :
                                                        (SimpleGraph.Subgraph.restrict G'').Adj v w G'.Adj v w G''.Adj v w
                                                        theorem SimpleGraph.Subgraph.coeSubgraph_injective {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) :
                                                        Function.Injective SimpleGraph.Subgraph.coeSubgraph
                                                        theorem SimpleGraph.Subgraph.coeSubgraph_le {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (H' : H.coe.Subgraph) :

                                                        Edge deletion #

                                                        def SimpleGraph.Subgraph.deleteEdges {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set (Sym2 V)) :
                                                        G.Subgraph

                                                        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.

                                                        Equations
                                                        • G'.deleteEdges s = { verts := G'.verts, Adj := G'.Adj \ Sym2.ToRel s, adj_sub := , edge_vert := , symm := }
                                                        Instances For
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_verts {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          (G'.deleteEdges s).verts = G'.verts
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) (v : V) (w : V) :
                                                          (G'.deleteEdges s).Adj v w G'.Adj v w s(v, w)s
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_deleteEdges {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) (s' : Set (Sym2 V)) :
                                                          (G'.deleteEdges s).deleteEdges s' = G'.deleteEdges (s s')
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_empty_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                          G'.deleteEdges = G'
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_spanningCoe_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          G'.spanningCoe.deleteEdges s = (G'.deleteEdges s).spanningCoe
                                                          theorem SimpleGraph.Subgraph.deleteEdges_coe_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 G'.verts)) :
                                                          G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe
                                                          theorem SimpleGraph.Subgraph.coe_deleteEdges_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)
                                                          theorem SimpleGraph.Subgraph.deleteEdges_le {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          G'.deleteEdges s G'
                                                          theorem SimpleGraph.Subgraph.deleteEdges_le_of_le {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set (Sym2 V)} {s' : Set (Sym2 V)} (h : s s') :
                                                          G'.deleteEdges s' G'.deleteEdges s
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          G'.deleteEdges (G'.edgeSet s) = G'.deleteEdges s
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          G'.deleteEdges (s G'.edgeSet) = G'.deleteEdges s
                                                          theorem SimpleGraph.Subgraph.coe_deleteEdges_le {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) :
                                                          (G'.deleteEdges s).coe G'.coe
                                                          theorem SimpleGraph.Subgraph.spanningCoe_deleteEdges_le {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set (Sym2 V)) :
                                                          (G'.deleteEdges s).spanningCoe G'.spanningCoe

                                                          Induced subgraphs #

                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.induce_verts {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) :
                                                          (G'.induce s).verts = s
                                                          @[simp]
                                                          theorem SimpleGraph.Subgraph.induce_adj {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) (u : V) (v : V) :
                                                          (G'.induce s).Adj u v = (u s v s G'.Adj u v)
                                                          def SimpleGraph.Subgraph.induce {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) :
                                                          G.Subgraph

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

                                                          Equations
                                                          • G'.induce s = { verts := s, Adj := fun (u v : V) => u s v s G'.Adj u v, adj_sub := , edge_vert := , symm := }
                                                          Instances For
                                                            theorem SimpleGraph.induce_eq_coe_induce_top {V : Type u} {G : SimpleGraph V} (s : Set V) :
                                                            SimpleGraph.induce s G = (.induce s).coe
                                                            theorem SimpleGraph.Subgraph.induce_mono {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G.Subgraph} {s : Set V} {s' : Set V} (hg : G' G'') (hs : s s') :
                                                            G'.induce s G''.induce s'
                                                            theorem SimpleGraph.Subgraph.induce_mono_left {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {G'' : G.Subgraph} {s : Set V} (hg : G' G'') :
                                                            G'.induce s G''.induce s
                                                            theorem SimpleGraph.Subgraph.induce_mono_right {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {s' : Set V} (hs : s s') :
                                                            G'.induce s G'.induce s'
                                                            @[simp]
                                                            theorem SimpleGraph.Subgraph.induce_empty {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                            G'.induce =
                                                            @[simp]
                                                            theorem SimpleGraph.Subgraph.induce_self_verts {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                            G'.induce G'.verts = G'
                                                            theorem SimpleGraph.Subgraph.le_induce_top_verts {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                            G' .induce G'.verts
                                                            theorem SimpleGraph.Subgraph.le_induce_union {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {s' : Set V} :
                                                            G'.induce s G'.induce s' G'.induce (s s')
                                                            theorem SimpleGraph.Subgraph.le_induce_union_left {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {s' : Set V} :
                                                            G'.induce s G'.induce (s s')
                                                            theorem SimpleGraph.Subgraph.le_induce_union_right {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {s' : Set V} :
                                                            G'.induce s' G'.induce (s s')
                                                            theorem SimpleGraph.Subgraph.singletonSubgraph_eq_induce {V : Type u} {G : SimpleGraph V} {v : V} :
                                                            G.singletonSubgraph v = .induce {v}
                                                            theorem SimpleGraph.Subgraph.subgraphOfAdj_eq_induce {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (hvw : G.Adj v w) :
                                                            G.subgraphOfAdj hvw = .induce {v, w}
                                                            @[reducible, inline]
                                                            abbrev SimpleGraph.Subgraph.deleteVerts {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (s : Set V) :
                                                            G.Subgraph

                                                            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.

                                                            Equations
                                                            • G'.deleteVerts s = G'.induce (G'.verts \ s)
                                                            Instances For
                                                              theorem SimpleGraph.Subgraph.deleteVerts_verts {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} :
                                                              (G'.deleteVerts s).verts = G'.verts \ s
                                                              theorem SimpleGraph.Subgraph.deleteVerts_adj {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {u : V} {v : V} :
                                                              (G'.deleteVerts s).Adj u v u G'.verts us v G'.verts vs G'.Adj u v
                                                              @[simp]
                                                              theorem SimpleGraph.Subgraph.deleteVerts_deleteVerts {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set V) (s' : Set V) :
                                                              (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s s')
                                                              @[simp]
                                                              theorem SimpleGraph.Subgraph.deleteVerts_empty {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} :
                                                              G'.deleteVerts = G'
                                                              theorem SimpleGraph.Subgraph.deleteVerts_le {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} :
                                                              G'.deleteVerts s G'
                                                              theorem SimpleGraph.Subgraph.deleteVerts_mono {V : Type u} {G : SimpleGraph V} {s : Set V} {G' : G.Subgraph} {G'' : G.Subgraph} (h : G' G'') :
                                                              G'.deleteVerts s G''.deleteVerts s
                                                              theorem SimpleGraph.Subgraph.deleteVerts_anti {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} {s' : Set V} (h : s s') :
                                                              G'.deleteVerts s' G'.deleteVerts s
                                                              @[simp]
                                                              theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_left_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} :
                                                              G'.deleteVerts (G'.verts s) = G'.deleteVerts s
                                                              @[simp]
                                                              theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_set_right_eq {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V} :
                                                              G'.deleteVerts (s G'.verts) = G'.deleteVerts s