Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax68.SeriesParallel

Series-parallel graphs

concepts/Lax68/SeriesParallel.lean · lax-68

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.

    Concept map

    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    A finite two-terminal series-parallel graph is built from a single terminal edge by series and parallel composition. The side conditions say that the composed graphs meet only at the intended terminals, and the final support condition excludes unused isolated vertices.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Series-parallel graphs
    6type: definition
    7---
    8A finite two-terminal series-parallel graph is built from a single terminal
    9edge by series and parallel composition. The side conditions say that the
    10composed graphs meet only at the intended terminals, and the final support
    11condition excludes unused isolated vertices.
    12-/
    13
    14set_option autoImplicit false
    15
    16namespace Lax68.SeriesParallel
    17
    18def edgeGraph {V : Type*} (s t : V) : SimpleGraph V :=
    19 SimpleGraph.fromRel fun u v =>
    20 (u = s ∧ v = t) ∨
    21 (u = t ∧ v = s)
    22
    23inductive TwoTerminal {V : Type*} : SimpleGraph V → V → V → Prop
    24 | edge (s t : V) (hne : s ≠ t) :
    25 TwoTerminal (edgeGraph s t) s t
    26 | series
    27 {G H : SimpleGraph V}
    28 {s m t : V}
    29 (left : TwoTerminal G s m)
    30 (right : TwoTerminal H m t)
    31 (meet :
    32 ∀ v,
    33 v ∈ G.support →
    34 v ∈ H.support →
    35 v = m) :
    36 TwoTerminal (G ⊔ H) s t
    37 | parallel
    38 {G H : SimpleGraph V}
    39 {s t : V}
    40 (left : TwoTerminal G s t)
    41 (right : TwoTerminal H s t)
    42 (meet :
    43 ∀ v,
    44 v ∈ G.support →
    45 v ∈ H.support →
    46 v = s ∨ v = t) :
    47 TwoTerminal (G ⊔ H) s t
    48
    49def IsSeriesParallel {V : Type*} (G : SimpleGraph V) : Prop :=
    50 ∃ s t,
    51 TwoTerminal G s t ∧
    52 G.support = Set.univ
    53
    54end Lax68.SeriesParallel
    55

    Builds on

    none

    Used by

    From Mathlib

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…