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

• SimpleGraph.edgeFinset is the Finset of edges in a graph, if edgeSet is finite
• SimpleGraph.neighborFinset is the Finset of vertices adjacent to a given vertex, if neighborSet is finite
• SimpleGraph.incidenceFinset is the Finset of edges containing a given vertex, if incidenceSet is finite

Naming conventions

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

Implementation notes

• A locally finite graph is one with instances Π v, Fintype (G.neighborSet v).
• Given instances DecidableRel G.Adj and Fintype V, then the graph is locally finite, too.

@[reducible, inline]

abbrev SimpleGraph.edgeFinset {V : Type u_1} (G : SimpleGraph V) [Fintype ↑G.edgeSet] : Finset (Sym2 V)

The edgeSet of the graph as a Finset.

Equations

• G.edgeFinset = G.edgeSet.toFinset

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₁ 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₁ 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₁ G₂ : SimpleGraph V} [Fintype ↑G₁.edgeSet] [Fintype ↑G₂.edgeSet] : G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂

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.

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.

@[simp]

theorem SimpleGraph.edgeFinset_bot {V : Type u_1} : ⊥.edgeFinset = ∅

@[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

@[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

@[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

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₂

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 V → Prop) (r : 𝕜) : Prop

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.edgeFinset → p (G.deleteEdges ↑s) → r ≤ ↑s.card

theorem SimpleGraph.deleteFar_iff {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [OrderedRing 𝕜] [Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜} [Fintype (Sym2 V)] : G.DeleteFar p r ↔ ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑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 V → Prop} {r : 𝕜} [Fintype (Sym2 V)] : G.DeleteFar p r → ∀ ⦃H : SimpleGraph V⦄ [inst : DecidableRel H.Adj], H ≤ G → p H → r ≤ ↑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 V → Prop} {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)] : Finset 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

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)] : v ∉ G.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

@[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] : Finset (Sym2 V)

This is the Finset version of incidenceSet.

Equations

• G.incidenceFinset v = (G.incidenceSet v).toFinset

@[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 (e : Sym2 V) => v ∈ e) 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))

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.

Equations

• G.IsRegularOfDegree d = ∀ (v : V), G.degree v = d

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

• G.neighborSetFintype v = Subtype.fintype fun (x : V) => x ∈ G.neighborSet v

theorem SimpleGraph.neighborFinset_eq_filter {V : Type u_1} (G : SimpleGraph V) [Fintype V] {v : V} [DecidableRel G.Adj] : G.neighborFinset v = Finset.filter (fun (w : V) => G.Adj v w) 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

• G.minDegree = WithTop.untop' 0 (Finset.image (fun (v : V) => G.degree v) Finset.univ).min

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

• G.maxDegree = Option.getD (Finset.image (fun (v : V) => G.degree v) Finset.univ).max 0

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 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 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 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 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 w : V} (h : v ≠ w) : Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2