Dominating sets

DefinitionDominating set#✓fully proved

A set \(S\) of vertices of a simple graph \(G\) dominates \(G\) when every vertex of \(G\) lies in \(S\) or is adjacent to some vertex of \(S\).

def IsDominating {V : Type*} (G : SimpleGraph V) (S : Set V) : Prop :=
  ∀ v : V, v ∈ S ∨ ∃ u ∈ S, G.Adj u v

Used by 10

Used byDomination number · Dominating sets are at least as large as the domination number · A minimum dominating set exists · Existence of independent dominating sets · Independent dominating set · Dominating rook placements · Dominating sets of the rook graph · Domination polynomial · The domination polynomial at one counts dominating sets · Dominating sets have no uncovered vertex

DefinitionIndependent dominating set#✓fully proved

A set \(S\) of vertices of a simple graph \(G\) is an independent dominating set of \(G\) when no two vertices of \(S\) are adjacent and \(S\) dominates \(G\).

def IsIndepDominating {V : Type*} (G : SimpleGraph V) (S : Set V) : Prop :=
  G.IsIndepSet S ∧ G.IsDominating S

Uses 1 · Used by 4

Statement usesDominating set

Used byA minimum independent dominating set exists · Existence of independent dominating sets · Independent domination number · Independent dominating sets are at least as large as the independent domination number

DefinitionDomination number#✓fully proved

For a simple graph \(G\) on a finite vertex set, the domination number of \(G\) is the least number of elements of a dominating set of \(G\).

noncomputable def dominationNumber {V : Type*} (G : SimpleGraph V)
    [Fintype V] : ℕ :=
  sInf {k : ℕ | ∃ S : Finset V, S.card = k ∧ G.IsDominating ↑S}

Uses 1 · Used by 2

Statement usesDominating set

Used byDominating sets are at least as large as the domination number · A minimum dominating set exists

DefinitionIndependent domination number#✓fully proved

For a simple graph \(G\) on a finite vertex set, the independent domination number of \(G\) is the least number of elements of an independent dominating set of \(G\).

noncomputable def indepDominationNumber {V : Type*} (G : SimpleGraph V)
    [Fintype V] : ℕ :=
  sInf {k : ℕ | ∃ S : Finset V, S.card = k ∧ G.IsIndepDominating ↑S}

Uses 1 · Used by 2

Statement usesIndependent dominating set

Used byA minimum independent dominating set exists · Independent dominating sets are at least as large as the independent domination number

TheoremExistence of independent dominating sets#✓fully proved

Every finite graph has an independent dominating set.

theorem exists_isIndepDominating {V : Type*} (G : SimpleGraph V) [Finite V] :
    ∃ S : Finset V, G.IsIndepDominating ↑S

Uses 2 · Used by 1

Statement usesIndependent dominating set

Proof usesDominating set

Used byA minimum independent dominating set exists

TheoremA minimum independent dominating set exists#✓fully proved

Every simple graph \(G\) on a finite vertex set has an independent dominating set whose number of elements equals the independent domination number of \(G\).

theorem exists_indepDominationNumber_eq_card {V : Type*} (G : SimpleGraph V)
    [Fintype V] :
    ∃ S : Finset V, S.card = G.indepDominationNumber ∧ G.IsIndepDominating ↑S

Uses 3

Statement usesIndependent dominating set · Independent domination number

Proof usesExistence of independent dominating sets

TheoremIndependent dominating sets are at least as large as the independent domination number#✓fully proved

Let \(G\) be a simple graph on a finite vertex set. If \(S\) is an independent dominating set of \(G\), then the independent domination number of \(G\) is at most the number of elements of \(S\).

theorem indepDominationNumber_le_card {V : Type*} (G : SimpleGraph V)
    [Fintype V] {S : Finset V} (hS : G.IsIndepDominating ↑S) :
    G.indepDominationNumber ≤ S.card

Uses 2

Statement usesIndependent dominating set · Independent domination number

TheoremA minimum dominating set exists#✓fully proved

Every simple graph \(G\) on a finite vertex set has a dominating set whose number of elements equals the domination number of \(G\).

theorem exists_dominationNumber_eq_card {V : Type*} (G : SimpleGraph V)
    [Fintype V] :
    ∃ S : Finset V, S.card = G.dominationNumber ∧ G.IsDominating ↑S

Uses 2

Statement usesDominating set · Domination number

TheoremDominating sets are at least as large as the domination number#✓fully proved

Let \(G\) be a simple graph on a finite vertex set. If \(S\) is a dominating set of \(G\), then the domination number of \(G\) is at most the number of elements of \(S\).

theorem dominationNumber_le_card {V : Type*} (G : SimpleGraph V)
    [Fintype V] {S : Finset V} (hS : G.IsDominating ↑S) :
    G.dominationNumber ≤ S.card

Uses 2

Statement usesDominating set · Domination number

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.