Dominating sets and domination numbers

This file introduces dominating sets and related invariants.

Main definitions

• SimpleGraph.IsDominating : A set of vertices that dominates all vertices.
• SimpleGraph.IsNDominatingSet : A dominating set with n vertices.
• SimpleGraph.dominationNumber : The domination number of a graph.
• SimpleGraph.IsTotalDominating : A total dominating set.
• SimpleGraph.IsTotalNDominatingSet : A total dominating set with n vertices.
• SimpleGraph.totalDominationNumber : The total domination number.

Future work should extend this file with connected, independent, and power variants as well as domination-related lemmas.

Dominating sets

def SimpleGraph.IsDominating {α : Type u_1} (G : SimpleGraph α) (D : Set α) : Prop

A set D is a dominating set for G if every vertex of G is either in D or adjacent to a vertex of D.

Equations

• G.IsDominating D = ∀ (v : α), v ∈ D ∨ ∃ w ∈ D, G.Adj v w

structure SimpleGraph.IsNDominatingSet {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (D : Finset α) : Prop

An n-dominating set is a dominating set with n vertices.

• isDominating : G.IsDominating ↑D
• card_eq : D.card = n

theorem SimpleGraph.isNDominatingSet_iff {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (D : Finset α) : IsNDominatingSet n D ↔ G.IsDominating ↑D ∧ D.card = n

Domination number

noncomputable def SimpleGraph.dominationNumber {α : Type u_1} (G : SimpleGraph α) : ℕ

The domination number of a graph G is the minimum size of a dominating set. It is 0 if there are no vertices.

Equations

• G.dominationNumber = sInf {n : ℕ | ∃ (D : Finset α), SimpleGraph.IsNDominatingSet n D}

def SimpleGraph.computable_dom_num {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ

Computable domination number via powerset enumeration.

Equations

• G.computable_dom_num = {D ∈ Finset.univ.powerset | ∀ (v : α), v ∈ D ∨ ∃ w ∈ D, G.Adj v w}.inf' ⋯ Finset.card

Total domination

def SimpleGraph.IsTotalDominating {α : Type u_1} (G : SimpleGraph α) (D : Set α) : Prop

A set D is a total dominating set if every vertex is adjacent to a vertex in D.

Equations

• G.IsTotalDominating D = ∀ (v : α), ∃ w ∈ D, G.Adj v w

structure SimpleGraph.IsTotalNDominatingSet {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (D : Finset α) : Prop

An n-total dominating set is a total dominating set with n vertices.

• isTotalDominating : G.IsTotalDominating ↑D
• card_eq : D.card = n

theorem SimpleGraph.isTotalNDominatingSet_iff {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (D : Finset α) : IsTotalNDominatingSet n D ↔ G.IsTotalDominating ↑D ∧ D.card = n

noncomputable def SimpleGraph.totalDominationNumber {α : Type u_1} (G : SimpleGraph α) : ℕ

The total domination number of G.

Equations

• G.totalDominationNumber = sInf {n : ℕ | ∃ (D : Finset α), SimpleGraph.IsTotalNDominatingSet n D}

Connected domination

def SimpleGraph.IsConnectedDominating {α : Type u_1} (G : SimpleGraph α) (D : Set α) : Prop

A set is a connected dominating set if it is dominating and induces a connected subgraph.

Equations

• G.IsConnectedDominating D = (G.IsDominating D ∧ (SimpleGraph.induce D G).Connected)

noncomputable def SimpleGraph.connectedDominationNumber {α : Type u_1} (G : SimpleGraph α) : ℕ

The connected domination number of G.

Equations

• G.connectedDominationNumber = sInf {n : ℕ | ∃ (D : Finset α), G.IsConnectedDominating ↑D ∧ D.card = n}

Independent domination

def SimpleGraph.IsIndepDominating {α : Type u_1} (G : SimpleGraph α) (D : Set α) : Prop

Equations

• G.IsIndepDominating D = (G.IsIndepSet D ∧ G.IsDominating D)

structure SimpleGraph.IsNIndepDominatingSet {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (D : Finset α) : Prop

• isIndep : G.IsIndepSet ↑D
• isDominating : G.IsDominating ↑D
• card_eq : D.card = n

theorem SimpleGraph.isNIndepDominatingSet_iff {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (D : Finset α) : IsNIndepDominatingSet n D ↔ G.IsIndepSet ↑D ∧ G.IsDominating ↑D ∧ D.card = n

noncomputable def SimpleGraph.indepDominationNumber {α : Type u_1} (G : SimpleGraph α) : ℕ

Equations

• G.indepDominationNumber = sInf {n : ℕ | ∃ (D : Finset α), SimpleGraph.IsNIndepDominatingSet n D}

Vertex and edge covers

def SimpleGraph.IsEdgeCover {α : Type u_1} (G : SimpleGraph α) (M : Set (Sym2 α)) : Prop

A set of edges is an edge cover if every vertex is incident to some edge in it.

Equations

• G.IsEdgeCover M = (M ⊆ G.edgeSet ∧ ∀ (v : α), ∃ e ∈ M, v ∈ e)

noncomputable def SimpleGraph.edgeCoverNumber {α : Type u_1} (G : SimpleGraph α) : ℕ

The minimum edge cover number of G.

Equations

• G.edgeCoverNumber = sInf {n : ℕ | ∃ (M : Finset (Sym2 α)), G.IsEdgeCover ↑M ∧ M.card = n}

Edge domination

def SimpleGraph.edgesAdjacent {α : Type u_1} (e e' : Sym2 α) : Prop

Equations

• SimpleGraph.edgesAdjacent e e' = ∃ v ∈ e, v ∈ e'

def SimpleGraph.IsEdgeDominating {α : Type u_1} (G : SimpleGraph α) (M : Set (Sym2 α)) : Prop

Equations

• G.IsEdgeDominating M = ∀ ⦃e : Sym2 α⦄, e ∈ G.edgeSet → e ∈ M ∨ ∃ e' ∈ M, SimpleGraph.edgesAdjacent e e'

structure SimpleGraph.IsNEdgeDominatingSet {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (M : Finset (Sym2 α)) : Prop

• isDominating : G.IsEdgeDominating ↑M
• card_eq : M.card = n

theorem SimpleGraph.isNEdgeDominatingSet_iff {α : Type u_1} {G : SimpleGraph α} (n : ℕ) (M : Finset (Sym2 α)) : IsNEdgeDominatingSet n M ↔ G.IsEdgeDominating ↑M ∧ M.card = n

noncomputable def SimpleGraph.edgeDominationNumber {α : Type u_1} (G : SimpleGraph α) : ℕ

Equations

• G.edgeDominationNumber = sInf {n : ℕ | ∃ (M : Finset (Sym2 α)), SimpleGraph.IsNEdgeDominatingSet n M}

Domination equivalence

theorem SimpleGraph.dom_num_eq_computable {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] : G.dominationNumber = G.computable_dom_num