Lax Lean Archive

Series-parallel graphs

Lax68.SeriesParallel · 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.

    Natural Language Statement

    Definition

    Series-parallel graph illustration
    Series-parallel graph illustration

    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.

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

    In the paper

    Lean source view on GitHub

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