HepLean Documentation

Mathlib.Combinatorics.SimpleGraph.Basic

Simple graphs #

This module defines simple graphs on a vertex type V as an irreflexive symmetric relation.

Main definitions #

TODO #

A variant of the aesop tactic for use in the graph library. Changes relative to standard aesop:

  • We use the SimpleGraph rule set in addition to the default rule sets.
  • We instruct Aesop's intro rule to unfold with default transparency.
  • We instruct Aesop to fail if it can't fully solve the goal. This allows us to use aesop_graph for auto-params.
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Use aesop_graph? to pass along a Try this suggestion when using aesop_graph

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      A variant of aesop_graph which does not fail if it is unable to solve the goal. Use this only for exploration! Nonterminal Aesop is even worse than nonterminal simp.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem SimpleGraph.ext {V : Type u} {x : SimpleGraph V} {y : SimpleGraph V} (Adj : x.Adj = y.Adj) :
        x = y
        theorem SimpleGraph.ext_iff {V : Type u} {x : SimpleGraph V} {y : SimpleGraph V} :
        x = y x.Adj = y.Adj
        structure SimpleGraph (V : Type u) :

        A simple graph is an irreflexive symmetric relation Adj on a vertex type V. The relation describes which pairs of vertices are adjacent. There is exactly one edge for every pair of adjacent vertices; see SimpleGraph.edgeSet for the corresponding edge set.

        Instances For
          theorem SimpleGraph.symm {V : Type u} (self : SimpleGraph V) :
          Symmetric self.Adj
          theorem SimpleGraph.loopless {V : Type u} (self : SimpleGraph V) :
          Irreflexive self.Adj
          @[simp]
          theorem SimpleGraph.mk'_apply_adj {V : Type u} (x : { adj : VVBool // (∀ (x y : V), adj x y = adj y x) ∀ (x : V), ¬adj x x = true }) (v : V) (w : V) :
          (SimpleGraph.mk' x).Adj v w = (x v w = true)
          def SimpleGraph.mk' {V : Type u} :
          { adj : VVBool // (∀ (x y : V), adj x y = adj y x) ∀ (x : V), ¬adj x x = true } SimpleGraph V

          Constructor for simple graphs using a symmetric irreflexive boolean function.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            We can enumerate simple graphs by enumerating all functions V → V → Bool and filtering on whether they are symmetric and irreflexive.

            Equations
            • instFintypeSimpleGraphOfDecidableEq = { elems := Finset.map SimpleGraph.mk' Finset.univ, complete := }

            There are finitely many simple graphs on a given finite type.

            Equations
            • =
            def SimpleGraph.fromRel {V : Type u} (r : VVProp) :

            Construct the simple graph induced by the given relation. It symmetrizes the relation and makes it irreflexive.

            Equations
            Instances For
              @[simp]
              theorem SimpleGraph.fromRel_adj {V : Type u} (r : VVProp) (v : V) (w : V) :
              (SimpleGraph.fromRel r).Adj v w v w (r v w r w v)

              The complete graph on a type V is the simple graph with all pairs of distinct vertices adjacent. In Mathlib, this is usually referred to as .

              Equations
              Instances For
                def emptyGraph (V : Type u) :

                The graph with no edges on a given vertex type V. Mathlib prefers the notation .

                Equations
                Instances For
                  @[simp]
                  theorem completeBipartiteGraph_adj (V : Type u_1) (W : Type u_2) (v : V W) (w : V W) :
                  (completeBipartiteGraph V W).Adj v w = (v.isLeft = true w.isRight = true v.isRight = true w.isLeft = true)
                  def completeBipartiteGraph (V : Type u_1) (W : Type u_2) :

                  Two vertices are adjacent in the complete bipartite graph on two vertex types if and only if they are not from the same side. Any bipartite graph may be regarded as a subgraph of one of these.

                  Equations
                  Instances For
                    @[simp]
                    theorem SimpleGraph.irrefl {V : Type u} (G : SimpleGraph V) {v : V} :
                    ¬G.Adj v v
                    theorem SimpleGraph.adj_comm {V : Type u} (G : SimpleGraph V) (u : V) (v : V) :
                    G.Adj u v G.Adj v u
                    theorem SimpleGraph.adj_symm {V : Type u} (G : SimpleGraph V) {u : V} {v : V} (h : G.Adj u v) :
                    G.Adj v u
                    theorem SimpleGraph.Adj.symm {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) :
                    G.Adj v u
                    theorem SimpleGraph.ne_of_adj {V : Type u} (G : SimpleGraph V) {a : V} {b : V} (h : G.Adj a b) :
                    a b
                    theorem SimpleGraph.Adj.ne {V : Type u} {G : SimpleGraph V} {a : V} {b : V} (h : G.Adj a b) :
                    a b
                    theorem SimpleGraph.Adj.ne' {V : Type u} {G : SimpleGraph V} {a : V} {b : V} (h : G.Adj a b) :
                    b a
                    theorem SimpleGraph.ne_of_adj_of_not_adj {V : Type u} (G : SimpleGraph V) {v : V} {w : V} {x : V} (h : G.Adj v x) (hn : ¬G.Adj w x) :
                    v w
                    @[simp]
                    theorem SimpleGraph.adj_inj {V : Type u} {G : SimpleGraph V} {H : SimpleGraph V} :
                    G.Adj = H.Adj G = H

                    The relation that one SimpleGraph is a subgraph of another. Note that this should be spelled .

                    Equations
                    • x.IsSubgraph y = ∀ ⦃v w : V⦄, x.Adj v wy.Adj v w
                    Instances For
                      instance SimpleGraph.instLE {V : Type u} :
                      Equations
                      • SimpleGraph.instLE = { le := SimpleGraph.IsSubgraph }
                      @[simp]
                      theorem SimpleGraph.isSubgraph_eq_le {V : Type u} :
                      SimpleGraph.IsSubgraph = fun (x1 x2 : SimpleGraph V) => x1 x2
                      instance SimpleGraph.instSup {V : Type u} :

                      The supremum of two graphs x ⊔ y has edges where either x or y have edges.

                      Equations
                      • SimpleGraph.instSup = { sup := fun (x y : SimpleGraph V) => { Adj := x.Adj y.Adj, symm := , loopless := } }
                      @[simp]
                      theorem SimpleGraph.sup_adj {V : Type u} (x : SimpleGraph V) (y : SimpleGraph V) (v : V) (w : V) :
                      (x y).Adj v w x.Adj v w y.Adj v w
                      instance SimpleGraph.instInf {V : Type u} :

                      The infimum of two graphs x ⊓ y has edges where both x and y have edges.

                      Equations
                      • SimpleGraph.instInf = { inf := fun (x y : SimpleGraph V) => { Adj := x.Adj y.Adj, symm := , loopless := } }
                      @[simp]
                      theorem SimpleGraph.inf_adj {V : Type u} (x : SimpleGraph V) (y : SimpleGraph V) (v : V) (w : V) :
                      (x y).Adj v w x.Adj v w y.Adj v w

                      We define Gᶜ to be the SimpleGraph V such that no two adjacent vertices in G are adjacent in the complement, and every nonadjacent pair of vertices is adjacent (still ensuring that vertices are not adjacent to themselves).

                      Equations
                      • SimpleGraph.hasCompl = { compl := fun (G : SimpleGraph V) => { Adj := fun (v w : V) => v w ¬G.Adj v w, symm := , loopless := } }
                      @[simp]
                      theorem SimpleGraph.compl_adj {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                      G.Adj v w v w ¬G.Adj v w
                      instance SimpleGraph.sdiff {V : Type u} :

                      The difference of two graphs x \ y has the edges of x with the edges of y removed.

                      Equations
                      • SimpleGraph.sdiff = { sdiff := fun (x y : SimpleGraph V) => { Adj := x.Adj \ y.Adj, symm := , loopless := } }
                      @[simp]
                      theorem SimpleGraph.sdiff_adj {V : Type u} (x : SimpleGraph V) (y : SimpleGraph V) (v : V) (w : V) :
                      (x \ y).Adj v w x.Adj v w ¬y.Adj v w
                      Equations
                      • SimpleGraph.supSet = { sSup := fun (s : Set (SimpleGraph V)) => { Adj := fun (a b : V) => Gs, G.Adj a b, symm := , loopless := } }
                      Equations
                      • SimpleGraph.infSet = { sInf := fun (s : Set (SimpleGraph V)) => { Adj := fun (a b : V) => (∀ ⦃G : SimpleGraph V⦄, G sG.Adj a b) a b, symm := , loopless := } }
                      @[simp]
                      theorem SimpleGraph.sSup_adj {V : Type u} {s : Set (SimpleGraph V)} {a : V} {b : V} :
                      (sSup s).Adj a b Gs, G.Adj a b
                      @[simp]
                      theorem SimpleGraph.sInf_adj {V : Type u} {a : V} {b : V} {s : Set (SimpleGraph V)} :
                      (sInf s).Adj a b (∀ Gs, G.Adj a b) a b
                      @[simp]
                      theorem SimpleGraph.iSup_adj {ι : Sort u_1} {V : Type u} {a : V} {b : V} {f : ιSimpleGraph V} :
                      (⨆ (i : ι), f i).Adj a b ∃ (i : ι), (f i).Adj a b
                      @[simp]
                      theorem SimpleGraph.iInf_adj {ι : Sort u_1} {V : Type u} {a : V} {b : V} {f : ιSimpleGraph V} :
                      (⨅ (i : ι), f i).Adj a b (∀ (i : ι), (f i).Adj a b) a b
                      theorem SimpleGraph.sInf_adj_of_nonempty {V : Type u} {a : V} {b : V} {s : Set (SimpleGraph V)} (hs : s.Nonempty) :
                      (sInf s).Adj a b Gs, G.Adj a b
                      theorem SimpleGraph.iInf_adj_of_nonempty {ι : Sort u_1} {V : Type u} {a : V} {b : V} [Nonempty ι] {f : ιSimpleGraph V} :
                      (⨅ (i : ι), f i).Adj a b ∀ (i : ι), (f i).Adj a b

                      For graphs G, H, G ≤ H iff ∀ a b, G.Adj a b → H.Adj a b.

                      Equations
                      Equations
                      @[simp]
                      theorem SimpleGraph.top_adj {V : Type u} (v : V) (w : V) :
                      .Adj v w v w
                      @[simp]
                      theorem SimpleGraph.bot_adj {V : Type u} (v : V) (w : V) :
                      .Adj v w False
                      @[simp]
                      theorem SimpleGraph.instInhabited_default (V : Type u) :
                      default =
                      Equations
                      • SimpleGraph.instUniqueOfSubsingleton = { default := , uniq := }
                      Equations
                      • =
                      instance SimpleGraph.Sup.adjDecidable (V : Type u) (G : SimpleGraph V) (H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] :
                      DecidableRel (G H).Adj
                      Equations
                      instance SimpleGraph.Inf.adjDecidable (V : Type u) (G : SimpleGraph V) (H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] :
                      DecidableRel (G H).Adj
                      Equations
                      instance SimpleGraph.Sdiff.adjDecidable (V : Type u) (G : SimpleGraph V) (H : SimpleGraph V) [DecidableRel G.Adj] [DecidableRel H.Adj] :
                      DecidableRel (G \ H).Adj
                      Equations
                      def SimpleGraph.support {V : Type u} (G : SimpleGraph V) :
                      Set V

                      G.support is the set of vertices that form edges in G.

                      Equations
                      Instances For
                        theorem SimpleGraph.mem_support {V : Type u} (G : SimpleGraph V) {v : V} :
                        v G.support ∃ (w : V), G.Adj v w
                        theorem SimpleGraph.support_mono {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G G') :
                        G.support G'.support
                        def SimpleGraph.neighborSet {V : Type u} (G : SimpleGraph V) (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
                          instance SimpleGraph.neighborSet.memDecidable {V : Type u} (G : SimpleGraph V) (v : V) [DecidableRel G.Adj] :
                          DecidablePred fun (x : V) => x G.neighborSet v
                          Equations

                          The edges of G consist of the unordered pairs of vertices related by G.Adj. This is the order embedding; for the edge set of a particular graph, see SimpleGraph.edgeSet.

                          The way edgeSet is defined is such that mem_edgeSet is proved by Iff.rfl. (That is, s(v, w) ∈ G.edgeSet is definitionally equal to G.Adj v w.)

                          Equations
                          Instances For
                            @[reducible, inline]
                            abbrev SimpleGraph.edgeSet {V : Type u} (G : SimpleGraph V) :
                            Set (Sym2 V)

                            G.edgeSet is the edge set for G. This is an abbreviation for edgeSetEmbedding G that permits dot notation.

                            Equations
                            Instances For
                              @[simp]
                              theorem SimpleGraph.mem_edgeSet {V : Type u} (G : SimpleGraph V) {v : V} {w : V} :
                              s(v, w) G.edgeSet G.Adj v w
                              theorem SimpleGraph.not_isDiag_of_mem_edgeSet {V : Type u} (G : SimpleGraph V) {e : Sym2 V} :
                              e G.edgeSet¬e.IsDiag
                              theorem SimpleGraph.edgeSet_inj {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} :
                              G₁.edgeSet = G₂.edgeSet G₁ = G₂
                              @[simp]
                              theorem SimpleGraph.edgeSet_subset_edgeSet {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} :
                              G₁.edgeSet G₂.edgeSet G₁ G₂
                              @[simp]
                              theorem SimpleGraph.edgeSet_ssubset_edgeSet {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} :
                              G₁.edgeSet G₂.edgeSet G₁ < G₂
                              theorem SimpleGraph.edgeSet_injective {V : Type u} :
                              Function.Injective SimpleGraph.edgeSet
                              theorem SimpleGraph.edgeSet_mono {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} :
                              G₁ G₂G₁.edgeSet G₂.edgeSet

                              Alias of the reverse direction of SimpleGraph.edgeSet_subset_edgeSet.

                              theorem SimpleGraph.edgeSet_strict_mono {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} :
                              G₁ < G₂G₁.edgeSet G₂.edgeSet

                              Alias of the reverse direction of SimpleGraph.edgeSet_ssubset_edgeSet.

                              @[simp]
                              theorem SimpleGraph.edgeSet_bot {V : Type u} :
                              .edgeSet =
                              @[simp]
                              theorem SimpleGraph.edgeSet_top {V : Type u} :
                              .edgeSet = {e : Sym2 V | ¬e.IsDiag}
                              @[simp]
                              theorem SimpleGraph.edgeSet_subset_setOf_not_isDiag {V : Type u} (G : SimpleGraph V) :
                              G.edgeSet {e : Sym2 V | ¬e.IsDiag}
                              @[simp]
                              theorem SimpleGraph.edgeSet_sup {V : Type u} (G₁ : SimpleGraph V) (G₂ : SimpleGraph V) :
                              (G₁ G₂).edgeSet = G₁.edgeSet G₂.edgeSet
                              @[simp]
                              theorem SimpleGraph.edgeSet_inf {V : Type u} (G₁ : SimpleGraph V) (G₂ : SimpleGraph V) :
                              (G₁ G₂).edgeSet = G₁.edgeSet G₂.edgeSet
                              @[simp]
                              theorem SimpleGraph.edgeSet_sdiff {V : Type u} (G₁ : SimpleGraph V) (G₂ : SimpleGraph V) :
                              (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet
                              @[simp]
                              theorem SimpleGraph.disjoint_edgeSet {V : Type u} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} :
                              Disjoint G₁.edgeSet G₂.edgeSet Disjoint G₁ G₂
                              @[simp]
                              theorem SimpleGraph.edgeSet_eq_empty {V : Type u} {G : SimpleGraph V} :
                              G.edgeSet = G =
                              @[simp]
                              theorem SimpleGraph.edgeSet_nonempty {V : Type u} {G : SimpleGraph V} :
                              G.edgeSet.Nonempty G
                              @[simp]
                              theorem SimpleGraph.edgeSet_sdiff_sdiff_isDiag {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)) :
                              G.edgeSet \ (s \ {e : Sym2 V | e.IsDiag}) = G.edgeSet \ s

                              This lemma, combined with edgeSet_sdiff and edgeSet_from_edgeSet, allows proving (G \ from_edgeSet s).edge_set = G.edgeSet \ s by simp.

                              theorem SimpleGraph.adj_iff_exists_edge {V : Type u} {G : SimpleGraph V} {v : V} {w : V} :
                              G.Adj v w v w eG.edgeSet, v e w e

                              Two vertices are adjacent iff there is an edge between them. The condition v ≠ w ensures they are different endpoints of the edge, which is necessary since when v = w the existential ∃ (e ∈ G.edgeSet), v ∈ e ∧ w ∈ e is satisfied by every edge incident to v.

                              theorem SimpleGraph.adj_iff_exists_edge_coe {V : Type u} {G : SimpleGraph V} {a : V} {b : V} :
                              G.Adj a b ∃ (e : G.edgeSet), e = s(a, b)
                              theorem SimpleGraph.edge_other_ne {V : Type u} (G : SimpleGraph V) {e : Sym2 V} (he : e G.edgeSet) {v : V} (h : v e) :
                              instance SimpleGraph.decidableMemEdgeSet {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] :
                              DecidablePred fun (x : Sym2 V) => x G.edgeSet
                              Equations
                              instance SimpleGraph.fintypeEdgeSet {V : Type u} (G : SimpleGraph V) [Fintype (Sym2 V)] [DecidableRel G.Adj] :
                              Fintype G.edgeSet
                              Equations
                              instance SimpleGraph.fintypeEdgeSetBot {V : Type u} :
                              Fintype .edgeSet
                              Equations
                              • SimpleGraph.fintypeEdgeSetBot = .mpr inferInstance
                              instance SimpleGraph.fintypeEdgeSetSup {V : Type u} (G₁ : SimpleGraph V) (G₂ : SimpleGraph V) [DecidableEq V] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
                              Fintype (G₁ G₂).edgeSet
                              Equations
                              • G₁.fintypeEdgeSetSup G₂ = .mpr inferInstance
                              instance SimpleGraph.fintypeEdgeSetInf {V : Type u} (G₁ : SimpleGraph V) (G₂ : SimpleGraph V) [DecidableEq V] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
                              Fintype (G₁ G₂).edgeSet
                              Equations
                              • G₁.fintypeEdgeSetInf G₂ = .mpr (G₁.edgeSet.fintypeInter G₂.edgeSet)
                              instance SimpleGraph.fintypeEdgeSetSdiff {V : Type u} (G₁ : SimpleGraph V) (G₂ : SimpleGraph V) [DecidableEq V] [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
                              Fintype (G₁ \ G₂).edgeSet
                              Equations
                              • G₁.fintypeEdgeSetSdiff G₂ = .mpr (G₁.edgeSet.fintypeDiff G₂.edgeSet)

                              fromEdgeSet constructs a SimpleGraph from a set of edges, without loops.

                              Equations
                              Instances For
                                @[simp]
                                theorem SimpleGraph.fromEdgeSet_adj {V : Type u} {v : V} {w : V} (s : Set (Sym2 V)) :
                                (SimpleGraph.fromEdgeSet s).Adj v w s(v, w) s v w
                                @[simp]
                                theorem SimpleGraph.edgeSet_fromEdgeSet {V : Type u} (s : Set (Sym2 V)) :
                                (SimpleGraph.fromEdgeSet s).edgeSet = s \ {e : Sym2 V | e.IsDiag}
                                @[simp]
                                @[simp]

                                Incidence set #

                                def SimpleGraph.incidenceSet {V : Type u} (G : SimpleGraph V) (v : V) :
                                Set (Sym2 V)

                                Set of edges incident to a given vertex, aka incidence set.

                                Equations
                                Instances For
                                  theorem SimpleGraph.incidenceSet_subset {V : Type u} (G : SimpleGraph V) (v : V) :
                                  G.incidenceSet v G.edgeSet
                                  theorem SimpleGraph.mk'_mem_incidenceSet_iff {V : Type u} (G : SimpleGraph V) {a : V} {b : V} {c : V} :
                                  s(b, c) G.incidenceSet a G.Adj b c (a = b a = c)
                                  theorem SimpleGraph.mk'_mem_incidenceSet_left_iff {V : Type u} (G : SimpleGraph V) {a : V} {b : V} :
                                  s(a, b) G.incidenceSet a G.Adj a b
                                  theorem SimpleGraph.mk'_mem_incidenceSet_right_iff {V : Type u} (G : SimpleGraph V) {a : V} {b : V} :
                                  s(a, b) G.incidenceSet b G.Adj a b
                                  theorem SimpleGraph.edge_mem_incidenceSet_iff {V : Type u} (G : SimpleGraph V) {a : V} {e : G.edgeSet} :
                                  e G.incidenceSet a a e
                                  theorem SimpleGraph.incidenceSet_inter_incidenceSet_subset {V : Type u} (G : SimpleGraph V) {a : V} {b : V} (h : a b) :
                                  G.incidenceSet a G.incidenceSet b {s(a, b)}
                                  theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_adj {V : Type u} (G : SimpleGraph V) {a : V} {b : V} (h : G.Adj a b) :
                                  G.incidenceSet a G.incidenceSet b = {s(a, b)}
                                  theorem SimpleGraph.adj_of_mem_incidenceSet {V : Type u} (G : SimpleGraph V) {a : V} {b : V} {e : Sym2 V} (h : a b) (ha : e G.incidenceSet a) (hb : e G.incidenceSet b) :
                                  G.Adj a b
                                  theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj {V : Type u} (G : SimpleGraph V) {a : V} {b : V} (h : ¬G.Adj a b) (hn : a b) :
                                  G.incidenceSet a G.incidenceSet b =
                                  instance SimpleGraph.decidableMemIncidenceSet {V : Type u} (G : SimpleGraph V) [DecidableEq V] [DecidableRel G.Adj] (v : V) :
                                  DecidablePred fun (x : Sym2 V) => x G.incidenceSet v
                                  Equations
                                  @[simp]
                                  theorem SimpleGraph.mem_neighborSet {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                  w G.neighborSet v G.Adj v w
                                  theorem SimpleGraph.not_mem_neighborSet_self {V : Type u} (G : SimpleGraph V) {a : V} :
                                  aG.neighborSet a
                                  @[simp]
                                  theorem SimpleGraph.mem_incidenceSet {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                  s(v, w) G.incidenceSet v G.Adj v w
                                  theorem SimpleGraph.mem_incidence_iff_neighbor {V : Type u} (G : SimpleGraph V) {v : V} {w : V} :
                                  s(v, w) G.incidenceSet v w G.neighborSet v
                                  theorem SimpleGraph.adj_incidenceSet_inter {V : Type u} (G : SimpleGraph V) {v : V} {e : Sym2 V} (he : e G.edgeSet) (h : v e) :
                                  G.incidenceSet v G.incidenceSet (Sym2.Mem.other h) = {e}
                                  theorem SimpleGraph.compl_neighborSet_disjoint {V : Type u} (G : SimpleGraph V) (v : V) :
                                  Disjoint (G.neighborSet v) (G.neighborSet v)
                                  theorem SimpleGraph.neighborSet_union_compl_neighborSet_eq {V : Type u} (G : SimpleGraph V) (v : V) :
                                  G.neighborSet v G.neighborSet v = {v}
                                  theorem SimpleGraph.card_neighborSet_union_compl_neighborSet {V : Type u} [Fintype V] (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v G.neighborSet v)] :
                                  (G.neighborSet v G.neighborSet v).toFinset.card = Fintype.card V - 1
                                  theorem SimpleGraph.neighborSet_compl {V : Type u} (G : SimpleGraph V) (v : V) :
                                  G.neighborSet v = (G.neighborSet v) \ {v}
                                  def SimpleGraph.commonNeighbors {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                  Set V

                                  The set of common neighbors between two vertices v and w in a graph G is the intersection of the neighbor sets of v and w.

                                  Equations
                                  • G.commonNeighbors v w = G.neighborSet v G.neighborSet w
                                  Instances For
                                    theorem SimpleGraph.commonNeighbors_eq {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                    G.commonNeighbors v w = G.neighborSet v G.neighborSet w
                                    theorem SimpleGraph.mem_commonNeighbors {V : Type u} (G : SimpleGraph V) {u : V} {v : V} {w : V} :
                                    u G.commonNeighbors v w G.Adj v u G.Adj w u
                                    theorem SimpleGraph.commonNeighbors_symm {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                    G.commonNeighbors v w = G.commonNeighbors w v
                                    theorem SimpleGraph.not_mem_commonNeighbors_left {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                    vG.commonNeighbors v w
                                    theorem SimpleGraph.not_mem_commonNeighbors_right {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                    wG.commonNeighbors v w
                                    theorem SimpleGraph.commonNeighbors_subset_neighborSet_left {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                    G.commonNeighbors v w G.neighborSet v
                                    theorem SimpleGraph.commonNeighbors_subset_neighborSet_right {V : Type u} (G : SimpleGraph V) (v : V) (w : V) :
                                    G.commonNeighbors v w G.neighborSet w
                                    instance SimpleGraph.decidableMemCommonNeighbors {V : Type u} (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (w : V) :
                                    DecidablePred fun (x : V) => x G.commonNeighbors v w
                                    Equations
                                    theorem SimpleGraph.commonNeighbors_top_eq {V : Type u} {v : V} {w : V} :
                                    .commonNeighbors v w = Set.univ \ {v, w}
                                    def SimpleGraph.otherVertexOfIncident {V : Type u} (G : SimpleGraph V) [DecidableEq V] {v : V} {e : Sym2 V} (h : e G.incidenceSet v) :
                                    V

                                    Given an edge incident to a particular vertex, get the other vertex on the edge.

                                    Equations
                                    Instances For
                                      theorem SimpleGraph.edge_other_incident_set {V : Type u} (G : SimpleGraph V) [DecidableEq V] {v : V} {e : Sym2 V} (h : e G.incidenceSet v) :
                                      e G.incidenceSet (G.otherVertexOfIncident h)
                                      theorem SimpleGraph.incidence_other_prop {V : Type u} (G : SimpleGraph V) [DecidableEq V] {v : V} {e : Sym2 V} (h : e G.incidenceSet v) :
                                      G.otherVertexOfIncident h G.neighborSet v
                                      theorem SimpleGraph.incidence_other_neighbor_edge {V : Type u} (G : SimpleGraph V) [DecidableEq V] {v : V} {w : V} (h : w G.neighborSet v) :
                                      G.otherVertexOfIncident = w
                                      @[simp]
                                      theorem SimpleGraph.incidenceSetEquivNeighborSet_apply_coe {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) (e : (G.incidenceSet v)) :
                                      ((G.incidenceSetEquivNeighborSet v) e) = G.otherVertexOfIncident
                                      @[simp]
                                      theorem SimpleGraph.incidenceSetEquivNeighborSet_symm_apply_coe {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) (w : (G.neighborSet v)) :
                                      ((G.incidenceSetEquivNeighborSet v).symm w) = s(v, w)
                                      def SimpleGraph.incidenceSetEquivNeighborSet {V : Type u} (G : SimpleGraph V) [DecidableEq V] (v : V) :
                                      (G.incidenceSet v) (G.neighborSet v)

                                      There is an equivalence between the set of edges incident to a given vertex and the set of vertices adjacent to the vertex.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        Edge deletion #

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

                                        Given a set of vertex pairs, remove all of the corresponding edges from the graph's edge set, if present.

                                        See also: SimpleGraph.Subgraph.deleteEdges.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem SimpleGraph.deleteEdges_adj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {s : Set (Sym2 V)} :
                                          (G.deleteEdges s).Adj v w G.Adj v w s(v, w)s
                                          @[simp]
                                          theorem SimpleGraph.deleteEdges_edgeSet {V : Type u} (G : SimpleGraph V) (G' : SimpleGraph V) :
                                          G.deleteEdges G'.edgeSet = G \ G'
                                          @[simp]
                                          theorem SimpleGraph.deleteEdges_deleteEdges {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) (s' : Set (Sym2 V)) :
                                          (G.deleteEdges s).deleteEdges s' = G.deleteEdges (s s')
                                          @[simp]
                                          theorem SimpleGraph.deleteEdges_empty {V : Type u} {G : SimpleGraph V} :
                                          G.deleteEdges = G
                                          @[simp]
                                          theorem SimpleGraph.deleteEdges_univ {V : Type u} {G : SimpleGraph V} :
                                          G.deleteEdges Set.univ =
                                          theorem SimpleGraph.deleteEdges_le {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) :
                                          G.deleteEdges s G
                                          theorem SimpleGraph.deleteEdges_anti {V : Type u} {G : SimpleGraph V} {s₁ : Set (Sym2 V)} {s₂ : Set (Sym2 V)} (h : s₁ s₂) :
                                          G.deleteEdges s₂ G.deleteEdges s₁
                                          theorem SimpleGraph.deleteEdges_mono {V : Type u} {G : SimpleGraph V} {H : SimpleGraph V} {s : Set (Sym2 V)} (h : G H) :
                                          G.deleteEdges s H.deleteEdges s
                                          @[simp]
                                          theorem SimpleGraph.deleteEdges_eq_self {V : Type u} {G : SimpleGraph V} {s : Set (Sym2 V)} :
                                          G.deleteEdges s = G Disjoint G.edgeSet s
                                          theorem SimpleGraph.deleteEdges_eq_inter_edgeSet {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) :
                                          G.deleteEdges s = G.deleteEdges (s G.edgeSet)
                                          theorem SimpleGraph.deleteEdges_sdiff_eq_of_le {V : Type u} {G : SimpleGraph V} {H : SimpleGraph V} (h : H G) :
                                          G.deleteEdges (G.edgeSet \ H.edgeSet) = H
                                          theorem SimpleGraph.edgeSet_deleteEdges {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) :
                                          (G.deleteEdges s).edgeSet = G.edgeSet \ s