Well totally dominated graphs

A total dominating set of G is a set S of vertices such that every vertex of G (including vertices in S) has a neighbor in S. A total dominating set S is minimal if no proper subset of S is also a total dominating set.

A graph G is well totally dominated if every minimal total dominating set has the same cardinality; equivalently, the total domination number equals the maximum cardinality of a minimal total dominating set.

The pendant vertices (also called leaves) of G are the vertices of degree 1.

def SimpleGraph.IsTotalDominatingSet {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Prop

A set S is a total dominating set of G if every vertex has a neighbor in S.

Equations

• G.IsTotalDominatingSet S = ∀ (v : α), ∃ w ∈ S, G.Adj v w

def SimpleGraph.IsMinimalTotalDominatingSet {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] (S : Finset α) : Prop

A total dominating set S is minimal if no proper subset of S is also a total dominating set.

Equations

• G.IsMinimalTotalDominatingSet S = (G.IsTotalDominatingSet S ∧ ∀ T ⊂ S, ¬G.IsTotalDominatingSet T)

def SimpleGraph.IsWellTotallyDominated {α : Type u_1} (G : SimpleGraph α) [DecidableRel G.Adj] : Prop

A graph G is well totally dominated if every minimal total dominating set has the same cardinality.

Equations

• G.IsWellTotallyDominated = ∀ (S T : Finset α), G.IsMinimalTotalDominatingSet S → G.IsMinimalTotalDominatingSet T → S.card = T.card

noncomputable def SimpleGraph.pendantVertices {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : Finset α

The set of pendant vertices (leaves) of G: vertices of degree 1.

Equations

• G.pendantVertices = {v : α | G.degree v = 1}