Lax Lean Archive

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

Pathwidth

Lax183560.Pathwidth · concepts/Lax183560/Pathwidth.lean · lax-183560

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 pathwidth of a graph is the minimum width of a path decomposition. The width of a path decomposition is the maximum bag size minus one. The empty graph has pathwidth zero.

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

    Lean source view on GitHub

    1import Lax183560.PathDecomposition
    2import Mathlib.Order.Lattice.Nat
    3
    4/-!
    5---
    6title: Pathwidth
    7type: definition
    8---
    9The pathwidth of a graph is the minimum width of a path decomposition.
    10The width of a path decomposition is the maximum bag size minus one.
    11The empty graph has pathwidth zero.
    12-/
    13
    14namespace Lax183560.Pathwidth
    15
    16open Lax183560.PathDecomposition
    17
    18/-- Existence of a path decomposition with bags of size at most `k + 1`. -/
    19def HasPathwidthAtMost {V : Type} (G : SimpleGraph V) (k : ℕ) : Prop :=
    20 ∃ D : PathDecomposition G, ∀ i, (D.bag i).card ≤ k + 1
    21
    22/-- The minimum path-decomposition width. -/
    23noncomputable def pathwidth {V : Type} [Fintype V] [DecidableEq V]
    24 (G : SimpleGraph V) : ℕ :=
    25 sInf {k | HasPathwidthAtMost G k}
    26
    27end Lax183560.Pathwidth
    28
    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…