Domination.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

22 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (4)

Imported by 2 files

def SimpleGraph.IsDominating 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 line 51 source
Source documentation
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.

no axioms what this means
Statement uses: SimpleGraph, Set
Proof uses: Or, Membership.mem, Exists, And, SimpleGraph.Adj
1 instances, coercions and auxiliary constants left out.
```
def IsDominating (G : SimpleGraph α) (D : Set α) : Prop :=
…
```
structure SimpleGraph.IsNDominatingSet An n-dominating set is a dominating set with n vertices line 56 source
Source documentation
An n-dominating set is a dominating set with n vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat, Finset
```
structure IsNDominatingSet (n : ℕ) (D : Finset α) : Prop where
…
```
def SimpleGraph.dominationNumber The domination number of a graph G is the minimum size of a dominating set line 64 source
Source documentation
The domination number of a graph G is the minimum size of a dominating set. It is 0 if there are no vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, SimpleGraph.IsNDominatingSet
1 instances, coercions and auxiliary constants left out.
```
noncomputable def dominationNumber (G : SimpleGraph α) : ℕ :=
…
```
def SimpleGraph.computable_dom_num Computable domination number via powerset enumeration line 68 source
Source documentation
Computable domination number via powerset enumeration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Nat
Proof uses: Finset.inf', Finset, Finset.filter, Or, Membership.mem, Exists, And, Finset.powerset, Finset.univ, Finset.card
9 instances, coercions and auxiliary constants left out.
```
def computable_dom_num (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ :=
…
```
def SimpleGraph.IsTotalDominating A set D is a total dominating set if every vertex is adjacent to a vertex in D line 80 source
Source documentation
A set D is a total dominating set if every vertex is adjacent to a vertex in D.

no axioms what this means
Statement uses: SimpleGraph, Set
Proof uses: Exists, And, Membership.mem, SimpleGraph.Adj
1 instances, coercions and auxiliary constants left out.
```
def IsTotalDominating (G : SimpleGraph α) (D : Set α) : Prop :=
…
```
structure SimpleGraph.IsTotalNDominatingSet An n-total dominating set is a total dominating set with n vertices line 85 source
Source documentation
An n-total dominating set is a total dominating set with n vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat, Finset
```
structure IsTotalNDominatingSet (n : ℕ) (D : Finset α) : Prop where
…
```
def SimpleGraph.totalDominationNumber The total domination number of G line 90 source
Source documentation
The total domination number of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, SimpleGraph.IsTotalNDominatingSet
1 instances, coercions and auxiliary constants left out.
```
noncomputable def totalDominationNumber (G : SimpleGraph α) : ℕ :=
…
```
def SimpleGraph.IsConnectedDominating A set is a connected dominating set if it is dominating and induces a connected subgraph line 97 source
Source documentation
A set is a connected dominating set if it is dominating and induces a connected subgraph.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Set
Proof uses: And, SimpleGraph.IsDominating, SimpleGraph.Connected, SimpleGraph.induce
1 instances, coercions and auxiliary constants left out.
```
def IsConnectedDominating (G : SimpleGraph α) (D : Set α) : Prop :=
…
```
def SimpleGraph.connectedDominationNumber The connected domination number of G line 101 source
Source documentation
The connected domination number of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, And, SimpleGraph.IsConnectedDominating, Eq, Finset.card
3 instances, coercions and auxiliary constants left out.
```
noncomputable def connectedDominationNumber (G : SimpleGraph α) : ℕ :=
…
```
def SimpleGraph.IsIndepDominating line 106 source
no axioms what this means
Statement uses: SimpleGraph, Set
Proof uses: And, SimpleGraph.IsIndepSet, SimpleGraph.IsDominating
structure SimpleGraph.IsNIndepDominatingSet line 110 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat, Finset
def SimpleGraph.indepDominationNumber line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, SimpleGraph.IsNIndepDominatingSet
1 instances, coercions and auxiliary constants left out.
def SimpleGraph.IsEdgeCover A set of edges is an edge cover if every vertex is incident to some edge in it line 121 source
Source documentation
A set of edges is an edge cover if every vertex is incident to some edge in it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Set, Sym2
Proof uses: And, LE.le, SimpleGraph.edgeSet, Exists, Membership.mem
4 instances, coercions and auxiliary constants left out.
```
def IsEdgeCover (G : SimpleGraph α) (M : Set (Sym2 α)) : Prop :=
…
```
def SimpleGraph.edgeCoverNumber The minimum edge cover number of G line 125 source
Source documentation
The minimum edge cover number of G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, Sym2, And, SimpleGraph.IsEdgeCover, Eq, Finset.card
3 instances, coercions and auxiliary constants left out.
```
noncomputable def edgeCoverNumber (G : SimpleGraph α) : ℕ :=
…
```
def SimpleGraph.edgesAdjacent line 130 source
standard axioms: Quot.sound, propext what this means
Statement uses: Sym2
Proof uses: Exists, And, Membership.mem
2 instances, coercions and auxiliary constants left out.
def SimpleGraph.IsEdgeDominating line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Set, Sym2
Proof uses: Membership.mem, SimpleGraph.edgeSet, Or, Exists, And, SimpleGraph.edgesAdjacent
1 instances, coercions and auxiliary constants left out.
structure SimpleGraph.IsNEdgeDominatingSet line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat, Finset, Sym2
def SimpleGraph.edgeDominationNumber line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat
Proof uses: InfSet.sInf, Set.ofPred, Exists, Finset, Sym2, SimpleGraph.IsNEdgeDominatingSet
1 instances, coercions and auxiliary constants left out.
theorem SimpleGraph.dom_num_eq_computable line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Eq, Nat, SimpleGraph.dominationNumber, SimpleGraph.computable_dom_num
Proof uses: id, InfSet.sInf, Set.ofPred, Exists, Finset, SimpleGraph.IsNDominatingSet, le_antisymm, Finset.inf', Finset.filter, Or, Membership.mem, And, Finset.powerset, Finset.univ, Finset.card, csInf_le, Exists.intro, Set, lowerBounds, OfNat.ofNat and 24 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma SimpleGraph.exists_isNDominatingSet_dominationNumber The set Finset.univ is a dominating set of any graph, so the set of sizes of dominating sets is nonempty and dominationNumber is attained by some dominating set line 168 source
Source documentation
The set Finset.univ is a dominating set of any graph, so the set of sizes of dominating sets is nonempty and dominationNumber is attained by some dominating set.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, SimpleGraph, Exists, Finset, SimpleGraph.IsNDominatingSet, SimpleGraph.dominationNumber
Proof uses: Set.Nonempty, Nat, Set.ofPred, Exists.intro, Membership.mem, Set, Finset.card, Finset.univ, SimpleGraph.IsNDominatingSet.mk, Or.inl, And, SimpleGraph.Adj, Finset.mem_univ, rfl, Nat.sInf_mem
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma exists_isNDominatingSet_dominationNumber
    (G : SimpleGraph α) :
    ∃ D : Finset α, G.IsNDominatingSet G.dominationNumber D := by
…
```
lemma SimpleGraph.dominationNumber_le_of_isDominating If D is a dominating set of G with n elements then γ(G) ≤ n line 177 source
Source documentation
If D is a dominating set of G with n elements then γ(G) ≤ n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SimpleGraph, Finset, SimpleGraph.IsDominating, LE.le, Nat, SimpleGraph.dominationNumber, Finset.card
Proof uses: Nat.sInf_le, Set.ofPred, Exists, SimpleGraph.IsNDominatingSet, Exists.intro, SimpleGraph.IsNDominatingSet.mk, rfl
5 instances, coercions and auxiliary constants left out.
```
lemma dominationNumber_le_of_isDominating
    (G : SimpleGraph α) (D : Finset α) (hD : G.IsDominating D) :
    G.dominationNumber ≤ D.card :=
…
```
theorem SimpleGraph.dominationNumber_le_dominationNumber_boxProd Projection bound: γ(G) ≤ γ(G □ H) whenever H has a vertex line 189 source
Source documentation
Projection bound: γ(G) ≤ γ(G □ H) whenever H has a vertex.
Projecting a dominating set of G □ H onto the first coordinate yields a dominating set of G of no larger size: a vertex (v, b) is dominated by some (w, c) with either v = w (so v lies in the projection) or G.Adj v w (so v is dominated by w in the projection).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, DecidableEq, Nonempty, SimpleGraph, LE.le, Nat, SimpleGraph.dominationNumber, Prod, SimpleGraph.boxProd
Proof uses: Finset, SimpleGraph.IsNDominatingSet, Exists, SimpleGraph.exists_isNDominatingSet_dominationNumber, SimpleGraph.IsDominating, Eq, Finset.card, le_trans, Finset.image, Prod.fst, SimpleGraph.dominationNumber_le_of_isDominating, Or, Membership.mem, Set, And, SimpleGraph.Adj, Prod.mk, Or.inl, Iff.mpr, Finset.mem_coe and 12 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem dominationNumber_le_dominationNumber_boxProd
    {β : Type*} [Fintype β] [DecidableEq β] [Nonempty β]
    (G : SimpleGraph α) (H : SimpleGraph β) :
    G.dominationNumber ≤ (G □ H).dominationNumber := by
…
```
Mentions: SimpleGraph.dominationNumber