Documentation

Mathlib.Combinatorics.SimpleGraph.Finite

Definitions for finite and locally finite graphs #

This file defines finite versions of edgeSet, neighborSet and incidenceSet and proves some of their basic properties. It also defines the notion of a locally finite graph, which is one whose vertices have finite degree.

The design for finiteness is that each definition takes the smallest finiteness assumption necessary. For example, SimpleGraph.neighborFinset v only requires that v have finitely many neighbors.

Main definitions #

Naming conventions #

If the vertex type of a graph is finite, we refer to its cardinality as CardVerts or card_verts.

Implementation notes #

@[reducible, inline]
abbrev SimpleGraph.edgeFinset {V : Type u_1} (G : SimpleGraph V) [Fintype G.edgeSet] :

The edgeSet of the graph as a Finset.

Equations
  • G.edgeFinset = G.edgeSet.toFinset
Instances For
    theorem SimpleGraph.coe_edgeFinset {V : Type u_1} (G : SimpleGraph V) [Fintype G.edgeSet] :
    G.edgeFinset = G.edgeSet
    theorem SimpleGraph.mem_edgeFinset {V : Type u_1} {G : SimpleGraph V} {e : Sym2 V} [Fintype G.edgeSet] :
    e G.edgeFinset e G.edgeSet
    theorem SimpleGraph.not_isDiag_of_mem_edgeFinset {V : Type u_1} {G : SimpleGraph V} {e : Sym2 V} [Fintype G.edgeSet] :
    e G.edgeFinset¬e.IsDiag
    theorem SimpleGraph.edgeFinset_inj {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
    G₁.edgeFinset = G₂.edgeFinset G₁ = G₂
    theorem SimpleGraph.edgeFinset_subset_edgeFinset {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
    G₁.edgeFinset G₂.edgeFinset G₁ G₂
    theorem SimpleGraph.edgeFinset_ssubset_edgeFinset {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
    G₁.edgeFinset G₂.edgeFinset G₁ < G₂
    theorem SimpleGraph.edgeFinset_mono {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
    G₁ G₂G₁.edgeFinset G₂.edgeFinset

    Alias of the reverse direction of SimpleGraph.edgeFinset_subset_edgeFinset.

    theorem SimpleGraph.edgeFinset_strict_mono {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
    G₁ < G₂G₁.edgeFinset G₂.edgeFinset

    Alias of the reverse direction of SimpleGraph.edgeFinset_ssubset_edgeFinset.

    @[simp]
    theorem SimpleGraph.edgeFinset_bot {V : Type u_1} :
    .edgeFinset =
    @[simp]
    theorem SimpleGraph.edgeFinset_sup {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] [Fintype (G₁ G₂).edgeSet] [DecidableEq V] :
    (G₁ G₂).edgeFinset = G₁.edgeFinset G₂.edgeFinset
    @[simp]
    theorem SimpleGraph.edgeFinset_inf {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] [DecidableEq V] :
    (G₁ G₂).edgeFinset = G₁.edgeFinset G₂.edgeFinset
    @[simp]
    theorem SimpleGraph.edgeFinset_sdiff {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] [DecidableEq V] :
    (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset
    theorem SimpleGraph.disjoint_edgeFinset {V : Type u_1} {G₁ : SimpleGraph V} {G₂ : SimpleGraph V} [Fintype G₁.edgeSet] [Fintype G₂.edgeSet] :
    Disjoint G₁.edgeFinset G₂.edgeFinset Disjoint G₁ G₂
    theorem SimpleGraph.edgeFinset_eq_empty {V : Type u_1} {G : SimpleGraph V} [Fintype G.edgeSet] :
    G.edgeFinset = G =
    theorem SimpleGraph.edgeFinset_nonempty {V : Type u_1} {G : SimpleGraph V} [Fintype G.edgeSet] :
    G.edgeFinset.Nonempty G
    theorem SimpleGraph.edgeFinset_card {V : Type u_1} {G : SimpleGraph V} [Fintype G.edgeSet] :
    G.edgeFinset.card = Fintype.card G.edgeSet
    @[simp]
    theorem SimpleGraph.edgeSet_univ_card {V : Type u_1} {G : SimpleGraph V} [Fintype G.edgeSet] :
    Finset.univ.card = G.edgeFinset.card
    @[simp]
    theorem SimpleGraph.edgeFinset_top {V : Type u_1} [Fintype V] [DecidableEq V] :
    .edgeFinset = Finset.filter (fun (e : Sym2 V) => ¬e.IsDiag) Finset.univ
    theorem SimpleGraph.card_edgeFinset_top_eq_card_choose_two {V : Type u_1} [Fintype V] [DecidableEq V] :
    .edgeFinset.card = (Fintype.card V).choose 2

    The complete graph on n vertices has n.choose 2 edges.

    theorem SimpleGraph.card_edgeFinset_le_card_choose_two {V : Type u_1} {G : SimpleGraph V} [Fintype G.edgeSet] [Fintype V] :
    G.edgeFinset.card (Fintype.card V).choose 2

    Any graph on n vertices has at most n.choose 2 edges.

    theorem SimpleGraph.edgeFinset_deleteEdges {V : Type u_1} (G : SimpleGraph V) [DecidableEq V] [Fintype G.edgeSet] (s : Finset (Sym2 V)) [Fintype (G.deleteEdges s).edgeSet] :
    (G.deleteEdges s).edgeFinset = G.edgeFinset \ s
    def SimpleGraph.DeleteFar {V : Type u_1} (G : SimpleGraph V) {𝕜 : Type u_2} [OrderedRing 𝕜] [Fintype G.edgeSet] (p : SimpleGraph VProp) (r : 𝕜) :

    A graph is r-delete-far from a property p if we must delete at least r edges from it to get a graph with the property p.

    Equations
    • G.DeleteFar p r = ∀ ⦃s : Finset (Sym2 V)⦄, s G.edgeFinsetp (G.deleteEdges s)r s.card
    Instances For
      theorem SimpleGraph.deleteFar_iff {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [OrderedRing 𝕜] [Fintype G.edgeSet] {p : SimpleGraph VProp} {r : 𝕜} [Fintype (Sym2 V)] :
      G.DeleteFar p r ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H Gp Hr G.edgeFinset.card - H.edgeFinset.card
      theorem SimpleGraph.DeleteFar.le_card_sub_card {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [OrderedRing 𝕜] [Fintype G.edgeSet] {p : SimpleGraph VProp} {r : 𝕜} [Fintype (Sym2 V)] :
      G.DeleteFar p r∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H Gp Hr G.edgeFinset.card - H.edgeFinset.card

      Alias of the forward direction of SimpleGraph.deleteFar_iff.

      theorem SimpleGraph.DeleteFar.mono {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [OrderedRing 𝕜] [Fintype G.edgeSet] {p : SimpleGraph VProp} {r₁ : 𝕜} {r₂ : 𝕜} (h : G.DeleteFar p r₂) (hr : r₁ r₂) :
      G.DeleteFar p r₁

      Finiteness at a vertex #

      This section contains definitions and lemmas concerning vertices that have finitely many adjacent vertices. We denote this condition by Fintype (G.neighborSet v).

      We define G.neighborFinset v to be the Finset version of G.neighborSet v. Use neighborFinset_eq_filter to rewrite this definition as a Finset.filter expression.

      def SimpleGraph.neighborFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :

      G.neighbors v is the Finset version of G.Adj v in case G is locally finite at v.

      Equations
      • G.neighborFinset v = (G.neighborSet v).toFinset
      Instances For
        theorem SimpleGraph.neighborFinset_def {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
        G.neighborFinset v = (G.neighborSet v).toFinset
        @[simp]
        theorem SimpleGraph.mem_neighborFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] (w : V) :
        w G.neighborFinset v G.Adj v w
        theorem SimpleGraph.not_mem_neighborFinset_self {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
        vG.neighborFinset v
        theorem SimpleGraph.neighborFinset_disjoint_singleton {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
        Disjoint (G.neighborFinset v) {v}
        theorem SimpleGraph.singleton_disjoint_neighborFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
        Disjoint {v} (G.neighborFinset v)
        def SimpleGraph.degree {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :

        G.degree v is the number of vertices adjacent to v.

        Equations
        • G.degree v = (G.neighborFinset v).card
        Instances For
          @[simp]
          theorem SimpleGraph.card_neighborFinset_eq_degree {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
          (G.neighborFinset v).card = G.degree v
          @[simp]
          theorem SimpleGraph.card_neighborSet_eq_degree {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
          Fintype.card (G.neighborSet v) = G.degree v
          theorem SimpleGraph.degree_pos_iff_exists_adj {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] :
          0 < G.degree v ∃ (w : V), G.Adj v w
          theorem SimpleGraph.degree_compl {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [Fintype (G.neighborSet v)] [Fintype V] :
          G.degree v = Fintype.card V - 1 - G.degree v
          instance SimpleGraph.incidenceSetFintype {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [DecidableEq V] :
          Fintype (G.incidenceSet v)
          Equations
          • G.incidenceSetFintype v = Fintype.ofEquiv (↑(G.neighborSet v)) (G.incidenceSetEquivNeighborSet v).symm
          def SimpleGraph.incidenceFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [DecidableEq V] :

          This is the Finset version of incidenceSet.

          Equations
          • G.incidenceFinset v = (G.incidenceSet v).toFinset
          Instances For
            @[simp]
            theorem SimpleGraph.card_incidenceSet_eq_degree {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [DecidableEq V] :
            Fintype.card (G.incidenceSet v) = G.degree v
            @[simp]
            theorem SimpleGraph.card_incidenceFinset_eq_degree {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [DecidableEq V] :
            (G.incidenceFinset v).card = G.degree v
            @[simp]
            theorem SimpleGraph.mem_incidenceFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [DecidableEq V] (e : Sym2 V) :
            e G.incidenceFinset v e G.incidenceSet v
            theorem SimpleGraph.incidenceFinset_eq_filter {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype (G.neighborSet v)] [DecidableEq V] [Fintype G.edgeSet] :
            G.incidenceFinset v = Finset.filter (fun (x : Sym2 V) => v x) G.edgeFinset
            @[reducible, inline]
            abbrev SimpleGraph.LocallyFinite {V : Type u_1} (G : SimpleGraph V) :
            Type u_1

            A graph is locally finite if every vertex has a finite neighbor set.

            Equations
            • G.LocallyFinite = ((v : V) → Fintype (G.neighborSet v))
            Instances For
              def SimpleGraph.IsRegularOfDegree {V : Type u_1} (G : SimpleGraph V) [G.LocallyFinite] (d : ) :

              A locally finite simple graph is regular of degree d if every vertex has degree d.

              Equations
              • G.IsRegularOfDegree d = ∀ (v : V), G.degree v = d
              Instances For
                theorem SimpleGraph.IsRegularOfDegree.degree_eq {V : Type u_1} {G : SimpleGraph V} [G.LocallyFinite] {d : } (h : G.IsRegularOfDegree d) (v : V) :
                G.degree v = d
                theorem SimpleGraph.IsRegularOfDegree.compl {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {k : } (h : G.IsRegularOfDegree k) :
                G.IsRegularOfDegree (Fintype.card V - 1 - k)
                instance SimpleGraph.neighborSetFintype {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) :
                Fintype (G.neighborSet v)
                Equations
                theorem SimpleGraph.neighborFinset_eq_filter {V : Type u_1} (G : SimpleGraph V) [Fintype V] {v : V} [DecidableRel G.Adj] :
                G.neighborFinset v = Finset.filter (G.Adj v) Finset.univ
                theorem SimpleGraph.neighborFinset_compl {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (v : V) :
                G.neighborFinset v = (G.neighborFinset v) \ {v}
                @[simp]
                theorem SimpleGraph.complete_graph_degree {V : Type u_1} [Fintype V] [DecidableEq V] (v : V) :
                .degree v = Fintype.card V - 1
                theorem SimpleGraph.bot_degree {V : Type u_1} [Fintype V] (v : V) :
                .degree v = 0
                theorem SimpleGraph.IsRegularOfDegree.top {V : Type u_1} [Fintype V] [DecidableEq V] :
                .IsRegularOfDegree (Fintype.card V - 1)
                def SimpleGraph.minDegree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] :

                The minimum degree of all vertices (and 0 if there are no vertices). The key properties of this are given in exists_minimal_degree_vertex, minDegree_le_degree and le_minDegree_of_forall_le_degree.

                Equations
                Instances For
                  theorem SimpleGraph.exists_minimal_degree_vertex {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] :
                  ∃ (v : V), G.minDegree = G.degree v

                  There exists a vertex of minimal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.

                  theorem SimpleGraph.minDegree_le_degree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) :
                  G.minDegree G.degree v

                  The minimum degree in the graph is at most the degree of any particular vertex.

                  theorem SimpleGraph.le_minDegree_of_forall_le_degree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] (k : ) (h : ∀ (v : V), k G.degree v) :
                  k G.minDegree

                  In a nonempty graph, if k is at most the degree of every vertex, it is at most the minimum degree. Note the assumption that the graph is nonempty is necessary as long as G.minDegree is defined to be a natural.

                  def SimpleGraph.maxDegree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] :

                  The maximum degree of all vertices (and 0 if there are no vertices). The key properties of this are given in exists_maximal_degree_vertex, degree_le_maxDegree and maxDegree_le_of_forall_degree_le.

                  Equations
                  Instances For
                    theorem SimpleGraph.exists_maximal_degree_vertex {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] :
                    ∃ (v : V), G.maxDegree = G.degree v

                    There exists a vertex of maximal degree. Note the assumption of being nonempty is necessary, as the lemma implies there exists a vertex.

                    theorem SimpleGraph.degree_le_maxDegree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) :
                    G.degree v G.maxDegree

                    The maximum degree in the graph is at least the degree of any particular vertex.

                    theorem SimpleGraph.maxDegree_le_of_forall_degree_le {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (k : ) (h : ∀ (v : V), G.degree v k) :
                    G.maxDegree k

                    In a graph, if k is at least the degree of every vertex, then it is at least the maximum degree.

                    theorem SimpleGraph.degree_lt_card_verts {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) :
                    G.degree v < Fintype.card V
                    theorem SimpleGraph.maxDegree_lt_card_verts {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] :
                    G.maxDegree < Fintype.card V

                    The maximum degree of a nonempty graph is less than the number of vertices. Note that the assumption that V is nonempty is necessary, as otherwise this would assert the existence of a natural number less than zero.

                    theorem SimpleGraph.card_commonNeighbors_le_degree_left {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) (w : V) :
                    Fintype.card (G.commonNeighbors v w) G.degree v
                    theorem SimpleGraph.card_commonNeighbors_le_degree_right {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) (w : V) :
                    Fintype.card (G.commonNeighbors v w) G.degree w
                    theorem SimpleGraph.card_commonNeighbors_lt_card_verts {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) (w : V) :
                    Fintype.card (G.commonNeighbors v w) < Fintype.card V
                    theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : V} {w : V} (h : G.Adj v w) :
                    Fintype.card (G.commonNeighbors v w) < G.degree v

                    If the condition G.Adj v w fails, then card_commonNeighbors_le_degree is the best we can do in general.

                    theorem SimpleGraph.card_commonNeighbors_top {V : Type u_1} [Fintype V] [DecidableEq V] {v : V} {w : V} (h : v w) :
                    Fintype.card (.commonNeighbors v w) = Fintype.card V - 2