Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Vertex clique cover number

Lax825442.VertexCliqueCover · concepts/Lax825442/VertexCliqueCover.lean · lax-825442

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The vertex clique cover number is the minimum number of cliques partitioning the vertices, equivalently the chromatic number of the complement. Each color class of the complement is a clique of the original graph. The complement is finite, so converting its chromatic number to a natural number loses no information. The empty graph has value zero.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
    2
    3/-!
    4---
    5title: Vertex clique cover number
    6type: definition
    7---
    8The vertex clique cover number is the minimum number of cliques partitioning
    9the vertices, equivalently the chromatic number of the complement.
    10Each color class of the complement is a clique of the original graph.
    11The complement is finite, so converting its chromatic number to a natural
    12number loses no information. The empty graph has value zero.
    13-/
    14
    15namespace Lax825442.VertexCliqueCover
    16
    17/-- The vertex clique cover number, expressed as the chromatic number of the
    18complement. -/
    19noncomputable def vertexCliqueCover {V : Type} [Fintype V] [DecidableEq V]
    20 (G : SimpleGraph V) : ℕ :=
    21 Gᶜ.chromaticNumber.toNat
    22
    23end Lax825442.VertexCliqueCover
    24
    25
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…