Graph theory

StructureSimple graph#

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.

SimpleGraph.{u} (V : Type u) : Type u
Sources
MathlibSimpleGraph
Used by 10
Used byKönigsberg Bridges Problem · The Friendship Theorem · Adjacency matrix · Degree-sum formula · Matching · Regularity lemma · Strongly regular graphs · Triangle counting lemma · Triangle removal lemma · Turán's theorem

TheoremDegree-sum formula#

The degree-sum formula. This is also known as the handshaking lemma, which might more specifically refer to SimpleGraph.even_card_odd_degree_vertices.

SimpleGraph.sum_degrees_eq_twice_card_edges.{u} {V : Type u} (G : SimpleGraph V) [Fintype V]
  [DecidableRel G.Adj] : ∑ v, G.degree v = 2 * G.edgeFinset.card
Sources
MathlibSimpleGraph.sum_degrees_eq_twice_card_edges
Uses 3 · Used by 1
Statement usesFinite set · Natural number · Simple graph
Used byTutte theorem

DefinitionMatching#

The subgraph M of G is a matching if every vertex of M is incident to exactly one edge in M. We say that the vertices in M.support are matched or saturated.

SimpleGraph.Subgraph.IsMatching.{u_1} {V : Type u_1} {G : SimpleGraph V} (M : G.Subgraph) : Prop
Sources
MathlibSimpleGraph.Subgraph.IsMatching
Uses 2 · Used by 1
Statement usesSet · Simple graph
Used byTutte theorem

DefinitionAdjacency matrix#

adjMatrix G α is the matrix A such that A i j = (1 : α) if i and j are adjacent in the simple graph G, and otherwise A i j = 0.

SimpleGraph.adjMatrix.{u_1, u_2} (α : Type u_1) {V : Type u_2} (G : SimpleGraph V)
  [DecidableRel G.Adj] [Zero α] [One α] : Matrix V V α
Sources
MathlibSimpleGraph.adjMatrix
Uses 3 · Used by 1
Statement usesNatural number · Ring-valued matrix · Simple graph
Used byThe Friendship Theorem

StructureStrongly regular graphs#

A graph is strongly regular with parameters n k ℓ μ if * its vertex set has cardinality n * it is regular with degree k * every pair of adjacent vertices has ℓ common neighbors * every pair of nonadjacent vertices has μ common neighbors

SimpleGraph.IsSRGWith.{u} {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj]
  (n k ℓ μ : ℕ) : Prop
Sources
MathlibSimpleGraph.IsSRGWith
Uses 3
Statement usesFinite set · Natural number · Simple graph

TheoremTurán's theorem#

Turán's theorem. turanGraph n r is, up to isomorphism, the unique r + 1-cliquefree Turán-maximal graph on n vertices.

SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph.{u_1} {V : Type u_1} [Fintype V]
  {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) :
  G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)
Sources
MathlibSimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph
Uses 5
Statement usesFinite set · Natural number · Simple graph
Proof usesFinite · Integer

TheoremRegularity lemma#

Effective Szemerédi Regularity Lemma: For any sufficiently large graph, there is an ε-uniform equipartition of bounded size (where the bound does not depend on the graph).

szemeredi_regularity.{u_1} {α : Type u_1} [DecidableEq α] [Fintype α] (G : SimpleGraph α)
  [DecidableRel G.Adj] {ε : ℝ} {l : ℕ} (hε : 0 < ε) (hl : l ≤ Fintype.card α) :
  ∃ P,
    P.IsEquipartition ∧
      l ≤ P.parts.card ∧ P.parts.card ≤ SzemerediRegularity.bound ε l ∧ P.IsUniform G ε
Sources
Mathlibszemeredi_regularity
Uses 5 · Used by 3
Statement usesLogarithm · Simple graph
Proof usesCardinal · Characteristic zero · Ordered ring
Used byCorners theorem · Roth's theorem · Triangle removal lemma

TheoremTriangle counting lemma#

The Triangle Counting Lemma. If G is a graph and s, t, u are disjoint sets of vertices such that each pair is ε-uniform and 2 * ε-dense, then G contains at least (1 - 2 * ε) * ε ^ 3 * |s| * |t| * |u| triangles.

SimpleGraph.triangle_counting.{u_1} {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ}
  {s t u : Finset α} [DecidableEq α] [Fintype α] (dst : 2 * ε ≤ ↑(G.edgeDensity s t))
  (ust : G.IsUniform ε s t) (hst : Disjoint s t) (dsu : 2 * ε ≤ ↑(G.edgeDensity s u))
  (usu : G.IsUniform ε s u) (hsu : Disjoint s u) (dtu : 2 * ε ≤ ↑(G.edgeDensity t u))
  (utu : G.IsUniform ε t u) (htu : Disjoint t u) :
  (1 - 2 * ε) * ε ^ 3 * ↑s.card * ↑t.card * ↑u.card ≤ ↑(G.cliqueFinset 3).card
Sources
MathlibSimpleGraph.triangle_counting
Uses 6 · Used by 3
Statement usesField \(\R\) of real numbers · Finite set · Order · Simple graph
Proof usesCharacteristic zero · Ordered ring
Used byCorners theorem · Roth's theorem · Triangle removal lemma

TheoremTriangle removal lemma#

Triangle Removal Lemma. If there are not too many triangles (on the order of (card α)^3) then they can all be removed by removing a few edges (on the order of (card α)^2).

SimpleGraph.triangle_removal.{u_1} {α : Type u_1} [DecidableEq α] [Fintype α] {G : SimpleGraph α}
  [DecidableRel G.Adj] {ε : ℝ}
  (hG : ↑(G.cliqueFinset 3).card < SimpleGraph.triangleRemovalBound ε * ↑(Fintype.card α) ^ 3) :
  ∃ G' ≤ G,
    ∃ x, ↑G.edgeFinset.card - ↑G'.edgeFinset.card < ε * ↑(Fintype.card α ^ 2) ∧ G'.CliqueFree 3
Sources
MathlibSimpleGraph.triangle_removal
Uses 5
Statement usesLogarithm · Simple graph
Proof usesCharacteristic p · Regularity lemma · Triangle counting lemma

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.