Lax Lean Archive

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

Path decompositions

Lax183560.PathDecomposition · concepts/Lax183560/PathDecomposition.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

    A path decomposition of a graph is a finite sequence of vertex bags such that every vertex belongs to a bag, both endpoints of every edge belong to a common bag, and the bags containing any fixed vertex form an interval. The sequence may be empty when the graph has no vertices.

    Concept map
    1 concept; 1 descendant hidden
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Path decompositions
    6type: definition
    7---
    8A path decomposition of a graph is a finite sequence of vertex bags such
    9that every vertex belongs to a bag, both endpoints of every edge belong to
    10a common bag, and the bags containing any fixed vertex form an interval.
    11The sequence may be empty when the graph has no vertices.
    12-/
    13
    14namespace Lax183560.PathDecomposition
    15
    16/-- A path decomposition indexed by a finite linear order. -/
    17structure PathDecomposition {V : Type} (G : SimpleGraph V) where
    18 length : ℕ
    19 bag : Fin length → Finset V
    20 vertex_mem_bag : ∀ v : V, ∃ i, v ∈ bag i
    21 edge_mem_bag : ∀ ⦃u v : V⦄, G.Adj u v →
    22 ∃ i, u ∈ bag i ∧ v ∈ bag i
    23 bag_indices_interval : ∀ v : V, ∀ i j l : Fin length,
    24 (i ≤ j ∧ j ≤ l ∧ v ∈ bag i ∧ v ∈ bag l) → v ∈ bag j
    25
    26
    27end Lax183560.PathDecomposition
    28
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…