Euler's formula and cycle rank

TheoremRemoving one element lowers cardinality by one#✓fully proved

Removing one element from a finite type lowers its cardinality by one. See also Mathlib's Fintype.card_subtype_compl.

theorem card_subtype_ne_add_one {α : Type*} [Finite α] (a : α) :
    Nat.card {x : α // x ≠ a} + 1 = Nat.card α

Used by 9

Used byJordan curve theorem · Bounded faces of a finite lattice graph are counted by its cycle rank · Adding an edge between two components merges them · Veblen's theorem step for unions of cycles · Euler's formula · Combinatorial Euler relation for finite graphs · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

TheoremAdding a new edge increases the edge count by one#✓fully proved

Adding a new edge increases the number of edges by one. This is the Set.ncard form of Mathlib's SimpleGraph.card_edgeFinset_sup_edge.

theorem card_edgeSet_sup_edge (G : SimpleGraph V) {a b : V} (hne : a ≠ b)
    (hadj : ¬ G.Adj a b) :
    (G ⊔ edge a b).edgeSet.ncard = G.edgeSet.ncard + 1

Used by 3

Used byBounded faces of a finite lattice graph are counted by its cycle rank · Veblen's theorem step for unions of cycles · Euler's formula

TheoremEdgeless graph has one component per vertex#✓fully proved

The edgeless graph has one component per vertex.

theorem card_components_bot :
    Nat.card (⊥ : SimpleGraph V).ConnectedComponent = Nat.card V

Used by 8

Used byJordan curve theorem · Bounded faces of a finite lattice graph are counted by its cycle rank · Veblen's theorem step for unions of cycles · Euler's formula · Combinatorial Euler relation for finite graphs · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionCycle rank of a finite graph#✓fully proved

The cycle rank (nullity, first Betti number) |E| + c - |V| of a finite graph, where c is the number of connected components.

noncomputable def nullity (G : SimpleGraph V) : ℕ :=
  (G.edgeSet.ncard + Nat.card G.ConnectedComponent) - Nat.card V

Used by 20

Used byBounded regions indexed by the cycle rank · Jordan curve theorem · Cycle rank one gives a unique bounded region · Jordan curve theorem for cycles: face count two · Bounded faces of a finite lattice graph are counted by its cycle rank · Bounded region count as cycle rank · Veblen's theorem step for unions of cycles · Euler's formula · Combinatorial Euler relation for finite graphs · Face count of a finite graph from its cycle rank · Cycle graph has cycle rank one · Lattice Jordan curve theorem for simple closed walks · Subgraph of a simple closed lattice walk has cycle rank one · Number of cells is at most the nullity of the skeleton · Euler characteristic at most 1 for a connected skeleton · Hopf's Umlaufsatz · Faithful discrete Jordan statement for the face count · Plus and minus box measures on \(\mathbb{Z}^2\) differ for large \(\beta\) · Peierls bound · Peierls' theorem

DefinitionFace count of a finite graph from its cycle rank#✓fully proved

The face count nullity G + 1. For a finite subgraph of ℤ² it is the number of faces, including the unbounded one (StatMech.Lattice.jed_faithfulDiscreteJordan counts the bounded ones); as a definition it is purely combinatorial.

noncomputable def faceCount (G : SimpleGraph V) : ℕ := nullity G + 1

Uses 1 · Used by 10

Statement usesCycle rank of a finite graph

Used byJordan curve theorem for cycles: face count two · Even-degree subgraphs have as many regions as their face count · Peeling a cycle from an even-degree subgraph · Bounded faces of a finite lattice graph are counted by its cycle rank · Veblen's theorem step for unions of cycles · Region step property for even-degree subgraphs · Veblen step property for even-degree subgraphs · Euler's formula · Euler's formula solved for the number of components · Combinatorial Euler relation for finite graphs

TheoremCombinatorial Euler relation for finite graphs#✓fully proved

The combinatorial Euler relation |V| + F = |E| + c + 1 for a finite graph, where F = faceCount G is defined from the cycle rank.

theorem euler_relation (G : SimpleGraph V) :
    Nat.card V + faceCount G = G.edgeSet.ncard + Nat.card G.ConnectedComponent + 1

Uses 4

Statement usesFace count of a finite graph from its cycle rank

Proof usesEdgeless graph has one component per vertex · Removing one element lowers cardinality by one · Cycle rank of a finite graph

TheoremConnected finite graph has at least \(|V| - 1\) edges#✓fully proved

A connected finite graph has at least |V| - 1 edges. This is the Fintype form of Mathlib's SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one.

theorem connected_card_edges_ge {G : SimpleGraph V} [Fintype V] [Fintype G.edgeSet]
    (hG : G.Connected) : Fintype.card V ≤ G.edgeFinset.card + 1

TheoremConnected graph with \(|V| - 1\) edges is acyclic, and conversely#✓fully proved

A connected finite graph has exactly |V| - 1 edges iff it is acyclic. See also Mathlib's SimpleGraph.isTree_iff_connected_and_card and SimpleGraph.IsTree.card_edgeFinset.

theorem connected_card_edges_eq_iff_isAcyclic {G : SimpleGraph V} [Fintype V]
    [Fintype G.edgeSet] (hG : G.Connected) :
    G.edgeFinset.card + 1 = Fintype.card V ↔ G.IsAcyclic

DefinitionCyclomatic number \(|E| + 1 - |V|\) of a finite graph#✓fully proved

The cyclomatic number |E| + 1 - |V| of a finite graph. For a connected graph it is the dimension of the cycle space. See StatMech.Lattice.nullity for the version for arbitrary finite graphs.

def cyclomaticNumber (G : SimpleGraph V) [Fintype V] [Fintype G.edgeSet] : ℕ :=
  (G.edgeFinset.card + 1) - Fintype.card V

DefinitionGraph stays connected with a given bridge after deleting edges#✓fully proved

After deleting the edges B', the graph A is connected and {a, b} is one of its bridges.

def ecc_DualCutModel (A : SimpleGraph V) (B' : Set (Sym2 V)) (a b : V) : Prop :=
  (A.deleteEdges B').Connected ∧
    s(a, b) ∈ (A.deleteEdges B').edgeSet ∧
    ¬ ((A.deleteEdges B').deleteEdges {s(a, b)}).Reachable a b

DefinitionVertices of the grid \((-n, n)^2\)#✓fully proved

The vertices of the grid [-n, n]².

noncomputable def boxVerts (n : ℕ) : Finset (Site 2) :=
  (Finset.Icc (-(n : ℤ)) (n : ℤ) ×ˢ Finset.Icc (-(n : ℤ)) (n : ℤ)).image
    (fun p => ![p.1, p.2])

Uses 1 · Used by 1

Statement usesSite of the hypercubic lattice

Used byEuler's formula for the grid graph \((-n, n)^2\)

DefinitionHorizontal edges of the grid \((-n, n)^2\)#✓fully proved

The horizontal edges of the grid [-n, n]².

noncomputable def hEdges (n : ℕ) : Finset (Sym2 (Site 2)) :=
  (Finset.Ico (-(n : ℤ)) (n : ℤ) ×ˢ Finset.Icc (-(n : ℤ)) (n : ℤ)).image
    (fun p => s(![p.1, p.2], ![p.1 + 1, p.2]))

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byEdges of the grid \((-n, n)^2\) · Euler's formula for the grid graph \((-n, n)^2\)

DefinitionVertical edges of the grid \((-n, n)^2\)#✓fully proved

The vertical edges of the grid [-n, n]².

noncomputable def vEdges (n : ℕ) : Finset (Sym2 (Site 2)) :=
  (Finset.Icc (-(n : ℤ)) (n : ℤ) ×ˢ Finset.Ico (-(n : ℤ)) (n : ℤ)).image
    (fun p => s(![p.1, p.2], ![p.1, p.2 + 1]))

Uses 1 · Used by 2

Statement usesSite of the hypercubic lattice

Used byEdges of the grid \((-n, n)^2\) · Euler's formula for the grid graph \((-n, n)^2\)

DefinitionEdges of the grid \((-n, n)^2\)#✓fully proved

The edges of the grid [-n, n]².

noncomputable def boxEdges (n : ℕ) : Finset (Sym2 (Site 2)) := hEdges n ∪ vEdges n

Uses 3 · Used by 1

Statement usesSite of the hypercubic lattice · Horizontal edges of the grid \((-n, n)^2\) · Vertical edges of the grid \((-n, n)^2\)

Used byEuler's formula for the grid graph \((-n, n)^2\)

DefinitionUnit squares of the grid \((-n, n)^2\)#✓fully proved

The unit squares of the grid [-n, n]², labelled by their lower left corners.

noncomputable def boxCells (n : ℕ) : Finset (ℤ × ℤ) :=
  Finset.Ico (-(n : ℤ)) (n : ℤ) ×ˢ Finset.Ico (-(n : ℤ)) (n : ℤ)

Used by 2

Used byEuler's formula for the grid graph \((-n, n)^2\) · Number of faces of the grid \((-n, n)^2\)

DefinitionNumber of faces of the grid \((-n, n)^2\)#✓fully proved

The number of faces of the grid [-n, n]²: its unit squares and the unbounded face.

noncomputable def boxFaceCount (n : ℕ) : ℕ := (boxCells n).card + 1

Uses 1 · Used by 1

Statement usesUnit squares of the grid \((-n, n)^2\)

Used byEuler's formula for the grid graph \((-n, n)^2\)

TheoremEuler's formula for the grid graph \((-n, n)^2\)#✓fully proved

Euler's formula V - E + F = 2 for the planar grid graph [-n, n]², with faces counted geometrically (unit squares plus the unbounded face).

theorem box_euler (n : ℕ) :
    (boxVerts n).card + boxFaceCount n = (boxEdges n).card + 2

Uses 7

Statement usesSite of the hypercubic lattice · Edges of the grid \((-n, n)^2\) · Number of faces of the grid \((-n, n)^2\) · Vertices of the grid \((-n, n)^2\)

Proof usesUnit squares of the grid \((-n, n)^2\) · Horizontal edges of the grid \((-n, n)^2\) · Vertical edges of the grid \((-n, n)^2\)

AbbreviationSquare lattice induced on the box \((-n, n)^2\)#✓fully proved

The subgraph of the square lattice induced on the box [-n, n]².

abbrev boxInduce (n : ℕ) := (hypercubicLattice 2).induce (box 2 n)

Uses 3

Statement usesSite of the hypercubic lattice · Box \((-n, n)^d\) in the hypercubic lattice · Hypercubic lattice \(\mathbb{Z}^d\)

TheoremEuler's formula#✓fully proved

Euler's formula for a finite graph with c connected components: |V| - |E| + F = 1 + c, where F = faceCount G.

Here F is defined as the cycle rank plus one, so the statement is the combinatorial Euler relation; it agrees with StatMech.Lattice.euler_relation_sub up to the order of the summands. That F counts the faces of a plane embedding is a separate statement; for finite subgraphs of the square lattice the bounded faces are counted in StatMech.Lattice.jed_faithfulDiscreteJordan. Reference: L. Euler, Elementa doctrinae solidorum (1758).

theorem euler_general (G : SimpleGraph V) :
    (Nat.card V : ℤ) - G.edgeSet.ncard + faceCount G
      = 1 + Nat.card G.ConnectedComponent

Uses 5 · Used by 1

Statement usesFace count of a finite graph from its cycle rank

Proof usesEdgeless graph has one component per vertex · Adding a new edge increases the edge count by one · Removing one element lowers cardinality by one · Cycle rank of a finite graph

Used byEuler's formula solved for the number of components

TheoremEuler's formula solved for the number of components#✓fully proved

Euler's formula solved for the number of components: c = |V| - |E| + F - 1.

theorem euler_general_disconnected_components (G : SimpleGraph V) :
    (Nat.card G.ConnectedComponent : ℤ)
      = (Nat.card V : ℤ) - G.edgeSet.ncard + faceCount G - 1

Uses 2

Statement usesFace count of a finite graph from its cycle rank

Proof usesEuler's formula

DefinitionNon-bridge edge of a graph#✓fully proved

e is an edge of A whose endpoints remain connected after e is deleted.

def tnse_IsNonBridgeEdge (A : SimpleGraph V) (e : Sym2 V) : Prop :=
  ∃ a b : V, e = s(a, b) ∧ s(a, b) ∈ A.edgeSet ∧ (A.deleteEdges {s(a, b)}).Reachable a b

Used by 1

Used bySuccessive deletion of non-bridge edges

DefinitionDeleting a list of edges from a graph#✓fully proved

A with the edges of the list L deleted.

def tnse_deleteList (A : SimpleGraph V) : List (Sym2 V) → SimpleGraph V
  | [] => A
  | e :: L => (tnse_deleteList A L).deleteEdges {e}

Used by 1

Used bySuccessive deletion of non-bridge edges

DefinitionSuccessive deletion of non-bridge edges#✓fully proved

Deleting the edges of L from the last to the first, each edge is a non-bridge at the moment it is deleted.

def tnse_AllNonBridge (A : SimpleGraph V) : List (Sym2 V) → Prop
  | [] => True
  | e :: L => tnse_IsNonBridgeEdge (tnse_deleteList A L) e ∧ tnse_AllNonBridge A L

Uses 2

Statement usesNon-bridge edge of a graph · Deleting a list of edges from a graph

DefinitionThree-step detour avoiding an edge#✓fully proved

The edge e = {a, b} has a three-step detour a, a', b', b in A none of whose edges is e or lies in L.

def tnse_HasTreeFreeDetour (A : SimpleGraph V) (L : List (Sym2 V)) (e : Sym2 V) : Prop :=
  ∃ a b a' b' : V, e = s(a, b) ∧ s(a, b) ∈ A.edgeSet ∧
    A.Adj a a' ∧ A.Adj a' b' ∧ A.Adj b' b ∧
    s(a, a') ≠ s(a, b) ∧ s(a', b') ≠ s(a, b) ∧ s(b', b) ≠ s(a, b) ∧
    s(a, a') ∉ L ∧ s(a', b') ∉ L ∧ s(b', b) ∉ L

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.