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 #

source
šŸ”ø coverage
def SimpleGraph.edgeFinset {V : Type u_1} (G : SimpleGraph V) [Fintype ā†‘G.edgeSet] :
Finset (Sym2 V)

The edgeSet of the graph as a Finset.

Instances For
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.coe_edgeFinset {V : Type u_1} (G : SimpleGraph V) [Fintype ā†‘G.edgeSet] :
    ā†‘G.edgeFinset = G.edgeSet
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.mem_edgeFinset {V : Type u_1} {G : SimpleGraph V} {e : Sym2 V} [Fintype ā†‘G.edgeSet] :
    e āˆˆ G.edgeFinset ā†” e āˆˆ G.edgeSet
    source
    šŸ“ coverage
    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
    source
    šŸ“ coverage
    theorem SimpleGraph.card_toFinset_mem_edgeFinset {V : Type u_1} {G : SimpleGraph V} [Fintype ā†‘G.edgeSet] [DecidableEq V] (e : ā†„G.edgeFinset) :
    (ā†‘e).toFinset.card = 2

    Mapping an edge to a finite set produces a finset of size 2.

    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_inj {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] :
    Gā‚.edgeFinset = Gā‚‚.edgeFinset ā†” Gā‚ = Gā‚‚
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_subset_edgeFinset {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] :
    Gā‚.edgeFinset āŠ† Gā‚‚.edgeFinset ā†” Gā‚ ā‰¤ Gā‚‚
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_ssubset_edgeFinset {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] :
    Gā‚.edgeFinset āŠ‚ Gā‚‚.edgeFinset ā†” Gā‚ < Gā‚‚
    source
    šŸ“ coverage
    theorem SimpleGraph.edgeFinset_mono {V : Type u_1} {Gā‚ 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.

    source
    šŸ“ coverage
    theorem SimpleGraph.edgeFinset_strict_mono {V : Type u_1} {Gā‚ 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.

    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_bot {V : Type u_1} :
    āŠ„.edgeFinset = āˆ…
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_sup {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] [Fintype ā†‘(Gā‚ āŠ” Gā‚‚).edgeSet] [DecidableEq V] :
    (Gā‚ āŠ” Gā‚‚).edgeFinset = Gā‚.edgeFinset āˆŖ Gā‚‚.edgeFinset
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_inf {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] [DecidableEq V] :
    (Gā‚ āŠ“ Gā‚‚).edgeFinset = Gā‚.edgeFinset āˆ© Gā‚‚.edgeFinset
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_sdiff {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] [DecidableEq V] :
    (Gā‚ \ Gā‚‚).edgeFinset = Gā‚.edgeFinset \ Gā‚‚.edgeFinset
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.disjoint_edgeFinset {V : Type u_1} {Gā‚ Gā‚‚ : SimpleGraph V} [Fintype ā†‘Gā‚.edgeSet] [Fintype ā†‘Gā‚‚.edgeSet] :
    Disjoint Gā‚.edgeFinset Gā‚‚.edgeFinset ā†” Disjoint Gā‚ Gā‚‚
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_eq_empty {V : Type u_1} {G : SimpleGraph V} [Fintype ā†‘G.edgeSet] :
    G.edgeFinset = āˆ… ā†” G = āŠ„
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_nonempty {V : Type u_1} {G : SimpleGraph V} [Fintype ā†‘G.edgeSet] :
    G.edgeFinset.Nonempty ā†” G ā‰  āŠ„
    source
    šŸ“ coverage
    theorem SimpleGraph.edgeFinset_card {V : Type u_1} {G : SimpleGraph V} [Fintype ā†‘G.edgeSet] :
    G.edgeFinset.card = Fintype.card ā†‘G.edgeSet
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.card_edgeSet {V : Type u_1} {G : SimpleGraph V} [Fintype ā†‘G.edgeSet] :
    Fintype.card ā†‘G.edgeSet = G.edgeFinset.card
    source
    šŸ“ coverage
    theorem SimpleGraph.edgeSet_univ_card {V : Type u_1} {G : SimpleGraph V} [Fintype ā†‘G.edgeSet] :
    Finset.univ.card = G.edgeFinset.card
    source
    šŸ“ coverage
    @[simp]
    theorem SimpleGraph.edgeFinset_top {V : Type u_1} [Fintype V] [DecidableEq V] :
    āŠ¤.edgeFinset = Sym2.diagSetį¶œ.toFinset
    source
    šŸ“ coverage
    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.

    source
    šŸ“ coverage
    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.

    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.

    source
    šŸ”ø coverage
    def SimpleGraph.neighborFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
    Finset V

    G.neighborFinset v is the Finset version of G.neighborSet v in case G is locally finite at v.

    Instances For
      source
      šŸ“ coverage
      theorem SimpleGraph.neighborFinset_def {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
      G.neighborFinset v = (G.neighborSet v).toFinset
      source
      šŸ“ coverage
      @[simp]
      theorem SimpleGraph.coe_neighborFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
      ā†‘(G.neighborFinset v) = G.neighborSet v
      source
      šŸ“ coverage
      @[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
      source
      šŸ“ coverage
      theorem SimpleGraph.notMem_neighborFinset_self {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
      v āˆ‰ G.neighborFinset v
      source
      šŸ“ coverage
      theorem SimpleGraph.neighborFinset_disjoint_singleton {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
      Disjoint (G.neighborFinset v) {v}
      source
      šŸ“ coverage
      theorem SimpleGraph.singleton_disjoint_neighborFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
      Disjoint {v} (G.neighborFinset v)
      source
      šŸ”ø coverage
      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.

      Instances For
        source
        šŸ“ coverage
        @[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
        source
        šŸ“ coverage
        @[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
        source
        šŸ“ coverage
        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
        source
        šŸ“ coverage
        theorem SimpleGraph.degree_pos_iff_nonempty {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ā†‘(G.neighborSet v)] :
        0 < G.degree v ā†” (G.neighborSet v).Nonempty
        source
        šŸ“ coverage
        theorem SimpleGraph.Adj.degree_pos_left {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ā†‘(G.neighborSet v)] {w : V} (h : G.Adj v w) :
        0 < G.degree v
        source
        šŸ“ coverage
        theorem SimpleGraph.Adj.degree_pos_right {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ā†‘(G.neighborSet v)] {w : V} (h : G.Adj w v) :
        0 < G.degree v
        source
        šŸ“ coverage
        theorem SimpleGraph.degree_pos_iff_mem_support {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
        0 < G.degree v ā†” v āˆˆ G.support
        source
        šŸ“ coverage
        theorem SimpleGraph.degree_eq_zero_iff_notMem_support {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] :
        G.degree v = 0 ā†” v āˆ‰ G.support
        source
        šŸ“ coverage
        @[simp]
        theorem SimpleGraph.degree_eq_zero_of_subsingleton {V : Type u_1} {G : SimpleGraph V} (v : V) [Fintype ā†‘(G.neighborSet v)] [Subsingleton V] :
        G.degree v = 0
        source
        šŸ“ coverage
        theorem SimpleGraph.degree_eq_one_iff_existsUnique_adj {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ā†‘(G.neighborSet v)] :
        G.degree v = 1 ā†” āˆƒ! w : V, G.Adj v w
        source
        šŸ“ coverage
        theorem SimpleGraph.nontrivial_of_degree_ne_zero {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ā†‘(G.neighborSet v)] (h : G.degree v ā‰  0) :
        Nontrivial V
        source
        šŸ“ coverage
        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
        source
        šŸ”ø coverage
        @[implicit_reducible]
        instance SimpleGraph.incidenceSetFintype {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] [DecidableEq V] :
        Fintype ā†‘(G.incidenceSet v)
        source
        šŸ”ø coverage
        def SimpleGraph.incidenceFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] [DecidableEq V] :
        Finset (Sym2 V)

        This is the Finset version of incidenceSet.

        Instances For
          source
          šŸ“ coverage
          @[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
          source
          šŸ“ coverage
          @[simp]
          theorem SimpleGraph.coe_incidenceFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] [DecidableEq V] :
          ā†‘(G.incidenceFinset v) = G.incidenceSet v
          source
          šŸ“ coverage
          @[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
          source
          šŸ“ coverage
          @[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
          source
          šŸ“ coverage
          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 = {e āˆˆ G.edgeFinset | v āˆˆ e}
          source
          šŸ“ coverage
          theorem SimpleGraph.incidenceFinset_subset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] [DecidableEq V] [Fintype ā†‘G.edgeSet] :
          G.incidenceFinset v āŠ† G.edgeFinset
          source
          šŸ“ coverage
          theorem SimpleGraph.degree_le_card_edgeFinset {V : Type u_1} (G : SimpleGraph V) (v : V) [Fintype ā†‘(G.neighborSet v)] [Fintype ā†‘G.edgeSet] :
          G.degree v ā‰¤ G.edgeFinset.card

          The degree of a vertex is at most the number of edges.

          source
          šŸ“ coverage
          theorem SimpleGraph.degree_le_of_le {V : Type u_1} {G : SimpleGraph V} {v : V} [Fintype ā†‘(G.neighborSet v)] {H : SimpleGraph V} [Fintype ā†‘(H.neighborSet v)] (hle : G ā‰¤ H) :
          G.degree v ā‰¤ H.degree v

          If G ā‰¤ H then G.degree v ā‰¤ H.degree v for any vertex v.

          source
          šŸ”ø coverage
          @[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.

          Instances For
            source
            šŸ”¹ coverage
            def SimpleGraph.IsRegularOfDegree {V : Type u_1} (G : SimpleGraph V) [G.LocallyFinite] (d : ā„•) :
            Prop

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

            Instances For
              source
              šŸ“ coverage
              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
              source
              šŸ“ coverage
              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)
              source
              šŸ”ø coverage
              @[implicit_reducible]
              instance SimpleGraph.neighborSetFintype {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v : V) :
              Fintype ā†‘(G.neighborSet v)
              source
              šŸ“ coverage
              theorem SimpleGraph.neighborFinset_eq_filter {V : Type u_1} (G : SimpleGraph V) [Fintype V] {v : V} [DecidableRel G.Adj] :
              G.neighborFinset v = {w : V | G.Adj v w}
              source
              šŸ“ coverage
              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}
              source
              šŸ“ coverage
              @[simp]
              theorem SimpleGraph.complete_graph_degree {V : Type u_1} [Fintype V] [DecidableEq V] (v : V) :
              (completeGraph V).degree v = Fintype.card V - 1
              source
              šŸ“ coverage
              @[simp]
              theorem SimpleGraph.bot_degree {V : Type u_1} [Fintype V] (v : V) :
              āŠ„.degree v = 0
              source
              šŸ“ coverage
              theorem SimpleGraph.IsRegularOfDegree.top {V : Type u_1} [Fintype V] [DecidableEq V] :
              āŠ¤.IsRegularOfDegree (Fintype.card V - 1)
              source
              šŸ”ø coverage
              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.

              Instances For
                source
                šŸ“ coverage
                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.

                source
                šŸ“ coverage
                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.

                source
                šŸ“ coverage
                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.

                source
                šŸ“ coverage
                @[simp]
                theorem SimpleGraph.minDegree_of_isEmpty {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [IsEmpty V] :
                G.minDegree = 0

                If there are no vertices then the minDegree is zero.

                source
                šŸ“ coverage
                theorem SimpleGraph.minDegree_le_minDegree {V : Type u_1} {G : SimpleGraph V} [Fintype V] {H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (hle : G ā‰¤ H) :
                G.minDegree ā‰¤ H.minDegree

                If G is a subgraph of H then G.minDegree ā‰¤ H.minDegree.

                source
                šŸ“ coverage
                theorem SimpleGraph.minDegree_lt_card {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Nonempty V] :
                G.minDegree < Fintype.card V

                In a nonempty graph, the minimal degree is less than the number of vertices.

                source
                šŸ”ø coverage
                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.

                Instances For
                  source
                  šŸ“ coverage
                  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.

                  source
                  šŸ“ coverage
                  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.

                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.maxDegree_of_isEmpty {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [IsEmpty V] :
                  G.maxDegree = 0
                  source
                  šŸ“ coverage
                  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.

                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.maxDegree_bot_eq_zero {V : Type u_1} [Fintype V] :
                  āŠ„.maxDegree = 0
                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.minDegree_le_maxDegree {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] :
                  G.minDegree ā‰¤ G.maxDegree
                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.minDegree_bot_eq_zero {V : Type u_1} [Fintype V] :
                  āŠ„.minDegree = 0
                  source
                  šŸ“ coverage
                  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
                  source
                  šŸ“ coverage
                  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.

                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_commonNeighbors_le_degree_left {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v w : V) :
                  Fintype.card ā†‘(G.commonNeighbors v w) ā‰¤ G.degree v
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_commonNeighbors_le_degree_right {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v w : V) :
                  Fintype.card ā†‘(G.commonNeighbors v w) ā‰¤ G.degree w
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_commonNeighbors_lt_card_verts {V : Type u_1} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] (v w : V) :
                  Fintype.card ā†‘(G.commonNeighbors v w) < Fintype.card V
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {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.

                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_commonNeighbors_top {V : Type u_1} [Fintype V] [DecidableEq V] {v w : V} (h : v ā‰  w) :
                  Fintype.card ā†‘(āŠ¤.commonNeighbors v w) = Fintype.card V - 2
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.Iso.card_edgeFinset_eq {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} (f : G ā‰ƒg G') [Fintype ā†‘G.edgeSet] [Fintype ā†‘G'.edgeSet] :
                  G.edgeFinset.card = G'.edgeFinset.card
                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.Iso.degree_eq {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} (f : G ā‰ƒg G') (x : V) [Fintype ā†‘(G.neighborSet x)] [Fintype ā†‘(G'.neighborSet (f x))] :
                  G'.degree (f x) = G.degree x
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.Iso.minDegree_eq {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] [Fintype W] [DecidableRel G'.Adj] (f : G ā‰ƒg G') :
                  G.minDegree = G'.minDegree
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.Iso.maxDegree_eq {V : Type u_1} {G : SimpleGraph V} {W : Type u_2} {G' : SimpleGraph W} [Fintype V] [DecidableRel G.Adj] [Fintype W] [DecidableRel G'.Adj] (f : G ā‰ƒg G') :
                  G.maxDegree = G'.maxDegree
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.edgeFinset_subset_sym2_of_support_subset {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : G.support āŠ† s) :
                  G.edgeFinset āŠ† s.toFinset.sym2
                  source
                  šŸ”ø coverage
                  @[implicit_reducible]
                  instance SimpleGraph.instDecidablePredMemSetSupport {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] :
                  DecidablePred fun (x : V) => x āˆˆ G.support
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.map_edgeFinset_induce {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] :
                  Finset.map (Function.Embedding.subtype fun (x : V) => x āˆˆ s).sym2Map (induce s G).edgeFinset = G.edgeFinset āˆ© s.toFinset.sym2
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.map_edgeFinset_induce_of_support_subset {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : G.support āŠ† s) :
                  Finset.map (Function.Embedding.subtype fun (x : V) => x āˆˆ s).sym2Map (induce s G).edgeFinset = G.edgeFinset
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_edgeFinset_induce_of_support_subset {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : G.support āŠ† s) :
                  (induce s G).edgeFinset.card = G.edgeFinset.card

                  If the support of the simple graph G is a subset of the set s, then the induced subgraph of s has the same number of edges as G.

                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_edgeFinset_induce_support {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] :
                  (induce G.support G).edgeFinset.card = G.edgeFinset.card
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.map_neighborFinset_induce {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] [DecidableEq V] (v : ā†‘s) :
                  Finset.map (Function.Embedding.subtype fun (x : V) => x āˆˆ s) ((induce s G).neighborFinset v) = G.neighborFinset ā†‘v āˆ© s.toFinset
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : ā†‘s} (h : G.neighborSet ā†‘v āŠ† s) :
                  Finset.map (Function.Embedding.subtype fun (x : V) => x āˆˆ s) ((induce s G).neighborFinset v) = G.neighborFinset ā†‘v
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.degree_induce_of_neighborSet_subset {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {v : ā†‘s} (h : G.neighborSet ā†‘v āŠ† s) :
                  (induce s G).degree v = G.degree ā†‘v

                  If the neighbor set of a vertex v is a subset of s, then the degree of the vertex in the induced subgraph of s is the same as in G.

                  source
                  šŸ“ coverage
                  theorem SimpleGraph.degree_induce_of_support_subset {V : Type u_1} {s : Set V} [DecidablePred fun (x : V) => x āˆˆ s] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : G.support āŠ† s) (v : ā†‘s) :
                  (induce s G).degree v = G.degree ā†‘v

                  If the support of the simple graph G is a subset of the set s, then the degree of vertices in the induced subgraph of s are the same as in G.

                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.degree_induce_support {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (v : ā†‘G.support) :
                  (induce G.support G).degree v = G.degree ā†‘v
                  source
                  šŸ“ coverage
                  @[simp]
                  theorem SimpleGraph.edgeFinset_map {V : Type u_1} [Fintype V] {W : Type u_2} [Fintype W] [DecidableEq W] (f : V ā†Ŗ W) (G : SimpleGraph V) [DecidableRel G.Adj] :
                  (SimpleGraph.map (ā‡‘f) G).edgeFinset = Finset.map f.sym2Map G.edgeFinset
                  source
                  šŸ“ coverage
                  theorem SimpleGraph.card_edgeFinset_map {V : Type u_1} [Fintype V] {W : Type u_2} [Fintype W] [DecidableEq W] (f : V ā†Ŗ W) (G : SimpleGraph V) [DecidableRel G.Adj] :
                  (SimpleGraph.map (ā‡‘f) G).edgeFinset.card = G.edgeFinset.card