Centered colorings

DefinitionCenter of a vertex set under a coloring#✓fully proved

Let \(\varphi\) be a proper vertex coloring of a simple graph \(G\), let \(s\) be a set of vertices of \(G\) and let \(v\) be a vertex of \(G\). Then \(v\) is a \(\varphi\)-center of \(s\) if \(v \in s\) and no other vertex of \(s\) has the color \(\varphi(v)\).

def IsPhiCenter (φ : G.Coloring C) (s : Set V) (v : V) : Prop :=
  v ∈ s ∧ ∀ w ∈ s, φ w = φ v → w = v

Used by 4

Used byCentered coloring · Injective colorings are centered · Centers via unique existence · A vertex is a center of its singleton

DefinitionCentered coloring#✓fully proved

A proper vertex coloring \(\varphi\) of a simple graph \(G\) is centered if, for every set \(s\) of vertices of \(G\) whose induced subgraph is connected, some vertex is a \(\varphi\)-center of \(s\).

Quantifying over vertex sets whose induced subgraph is connected suffices: adding all induced edges on the same vertices keeps a connected subgraph connected, and whether a color occurs exactly once depends only on the vertex set together with the coloring.

def IsCentered (φ : G.Coloring C) : Prop :=
  ∀ s : Set V, (G.induce s).Connected → ∃ v, IsPhiCenter φ s v

Uses 1 · Used by 2

Statement usesCenter of a vertex set under a coloring

Used byInjective colorings are centered · The identity coloring is centered

TheoremCenters via unique existence#✓fully proved

Let \(\varphi\) be a proper vertex coloring of a simple graph \(G\), let \(s\) be a set of vertices of \(G\) and let \(v\) be a vertex of \(G\). Then \(v\) is a \(\varphi\)-center of \(s\) if and only if \(v \in s\) and there is exactly one vertex \(u \in s\) with \(\varphi(u) = \varphi(v)\).

theorem isPhiCenter_iff_existsUnique (φ : G.Coloring C) (s : Set V) (v : V) :
    IsPhiCenter φ s v ↔ v ∈ s ∧ ∃! u, u ∈ s ∧ φ u = φ v

Uses 1

Statement usesCenter of a vertex set under a coloring

TheoremA vertex is a center of its singleton#✓fully proved

For every proper vertex coloring \(\varphi\) of a simple graph \(G\) and every vertex \(v\) of \(G\), \(v\) is a \(\varphi\)-center of \(\{v\}\).

theorem isPhiCenter_singleton (φ : G.Coloring C) (v : V) :
    IsPhiCenter φ {v} v

Uses 1

Statement usesCenter of a vertex set under a coloring

TheoremInjective colorings are centered#✓fully proved

Every injective proper vertex coloring of a simple graph is centered: any vertex of a set whose induced subgraph is connected is a center of that set.

theorem isCentered_of_injective (φ : G.Coloring C)
    (hinj : Function.Injective ⇑φ) : IsCentered φ

Uses 2 · Used by 1

Statement usesCentered coloring

Proof usesCenter of a vertex set under a coloring

Used byThe identity coloring is centered

TheoremThe identity coloring is centered#✓fully proved

For every simple graph \(G\) with vertex set \(V\), the proper vertex coloring of \(G\) by \(V\) that gives each vertex itself as its color is centered.

theorem selfColoring_isCentered (G : SimpleGraph V) :
    IsCentered (SimpleGraph.selfColoring G)

Uses 2

Statement usesCentered coloring

Proof usesInjective colorings are centered

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.