Lax Lean Archive

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

Clique-width

Lax825442.CliqueWidth · concepts/Lax825442/CliqueWidth.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

    Clique-width is the least number of labels in a valid expression that builds the graph from vertex creation, disjoint union, joining two label classes, and relabelling. The expression language is imported from the registered Lax concept Lax271696.CliqueExprLax271696.CliqueExpr. A finite vertex type is transported to FinnFin n because that expression language uses canonically numbered vertices.

    Concept map
    2 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax271696.CliqueExpr
    2import Mathlib.Combinatorics.SimpleGraph.Maps
    3import Mathlib.Data.Fintype.EquivFin
    4import Mathlib.Order.Lattice.Nat
    5
    6/-!
    7---
    8title: Clique-width
    9type: definition
    10---
    11Clique-width is the least number of labels in a valid expression that builds
    12the graph from vertex creation, disjoint union, joining two label classes,
    13and relabelling. The expression language is imported from the registered
    14Lax concept `Lax271696.CliqueExpr`. A finite vertex type is transported to
    15`Fin n` because that expression language uses canonically numbered vertices.
    16-/
    17
    18namespace Lax825442.CliqueWidth
    19
    20open Lax271696.CliqueExpr
    21
    22/-- A valid `k`-expression builds a numbered copy of `G`. -/
    23def HasCliqueWidthAtMost {V : Type} [Fintype V] [DecidableEq V]
    24 (G : SimpleGraph V) (k : ℕ) : Prop :=
    25 Fintype.card V = 0 ∨
    26 ∃ e : Expr (Fintype.card V) k,
    27 ValidFor e (G.comap (Fintype.equivFin V).symm)
    28
    29/-- The minimum number of labels in a valid expression for `G`. -/
    30noncomputable def cliqueWidth {V : Type} [Fintype V] [DecidableEq V]
    31 (G : SimpleGraph V) : ℕ :=
    32 sInf {k | HasCliqueWidthAtMost G k}
    33
    34end Lax825442.CliqueWidth
    35
    36
    Builds on
    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…