Documentation

TauCeti.Combinatorics.Graph.Orientation.Indegree

Indegrees and outdegrees of multigraph orientations #

The indegree of a vertex under an orientation of a multigraph with finitely many actual edges counts the actual edges whose chosen head is that vertex; the outdegree counts those whose chosen tail is that vertex. Parallel edges are counted separately and a loop contributes one to each. Reversal exchanges the two counts, and summing either over all vertices counts every edge once.

On a vertex set S, the total indegree lies between the number of edges internal to S and the number of edges incident with S: an internal edge has its head in S, and an edge with its head in S is incident with S. These are the necessary conditions of the prescribed and bounded indegree theorems.

Main declarations #

source
noncomputable def Graph.Orientation.indegree {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (o : G.Orientation) (v : ↑G.vertexSet) :
ℕ

The number of actual edges whose chosen head is v. A loop at v counts once.

Instances For
    source
    noncomputable def Graph.Orientation.outdegree {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (o : G.Orientation) (v : ↑G.vertexSet) :
    ℕ

    The number of actual edges whose chosen tail is v. A loop at v counts once.

    Instances For
      source
      theorem Graph.Orientation.indegree_def {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] [DecidableEq ↑G.vertexSet] (o : G.Orientation) (v : ↑G.vertexSet) :
      o.indegree v = {e : ↑G.edgeSet | o.head e = v}.card
      source
      theorem Graph.Orientation.outdegree_def {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] [DecidableEq ↑G.vertexSet] (o : G.Orientation) (v : ↑G.vertexSet) :
      o.outdegree v = {e : ↑G.edgeSet | o.tail e = v}.card
      source
      @[simp]
      theorem Graph.Orientation.indegree_reverse {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (o : G.Orientation) (v : ↑G.vertexSet) :
      o.reverse.indegree v = o.outdegree v
      source
      @[simp]
      theorem Graph.Orientation.outdegree_reverse {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (o : G.Orientation) (v : ↑G.vertexSet) :
      o.reverse.outdegree v = o.indegree v
      source
      theorem Graph.Orientation.exists_outdegree_iff_exists_indegree {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (P : (↑G.vertexSet → ℕ) → Prop) :
      (∃ (o : G.Orientation), P o.outdegree) ↔ ∃ (o : G.Orientation), P o.indegree

      Reversal turns any condition on outdegrees into the same condition on indegrees.

      source
      theorem Graph.Orientation.sum_indegree_eq_card_filter {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] [DecidableEq ↑G.vertexSet] (o : G.Orientation) (S : Finset ↑G.vertexSet) :
      ∑ v ∈ S, o.indegree v = {e : ↑G.edgeSet | o.head e ∈ S}.card

      The total indegree on S counts the actual edges whose head lies in S.

      source
      theorem Graph.Orientation.sum_indegree {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] (o : G.Orientation) :
      ∑ v : ↑G.vertexSet, o.indegree v = Fintype.card ↑G.edgeSet

      The indegrees of an orientation sum to the number of actual edges, loops included.

      source
      theorem Graph.Orientation.sum_outdegree {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] [Fintype ↑G.vertexSet] (o : G.Orientation) :
      ∑ v : ↑G.vertexSet, o.outdegree v = Fintype.card ↑G.edgeSet

      The outdegrees of an orientation sum to the number of actual edges, loops included.

      source
      theorem Graph.Orientation.card_internalEdges_le_sum_indegree {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (o : G.Orientation) (S : Finset ↑G.vertexSet) :
      (G.internalEdges S).card ≤ ∑ v ∈ S, o.indegree v

      Every edge internal to S has its head in S, so it is counted by the total indegree on S.

      source
      theorem Graph.Orientation.sum_indegree_le_card_incidentEdges {V : Type u} {E : Type v} {G : Graph V E} [Fintype ↑G.edgeSet] (o : G.Orientation) (S : Finset ↑G.vertexSet) :
      ∑ v ∈ S, o.indegree v ≤ (G.incidentEdges S).card

      Every edge with its head in S is incident with S, so the total indegree on S is at most the number of edges incident with S.