Lax Lean Archive

Row and column graphs

Lax762056.ColumnGraph · concepts/Lax762056/ColumnGraph.lean · lax-762056

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

    For a row set RR and cc columns, the graph has vertices (r,j,s)∈R×{0,…,c−1}×{0,1}(r,j,s)\in R\times\{0,\ldots,c-1\}\times\{0,1\}. Each column induces a complete bipartite graph between its two sides. Within a row, every vertex is adjacent to both vertices in each consecutive column. There are no other edges.

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

    In the paper

    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Basic
    2
    3/-!
    4---
    5title: Row and column graphs
    6type: definition
    7---
    8For a row set RR and cc columns, the graph has vertices
    9(r,j,s)∈R×{0,…,c−1}×{0,1}(r,j,s)\in R\times\{0,\ldots,c-1\}\times\{0,1\}. Each column induces a
    10complete bipartite graph between its two sides. Within a row, every vertex
    11is adjacent to both vertices in each consecutive column. There are no other
    12edges.
    13-/
    14
    15namespace Lax762056.ColumnGraph
    16
    17open SimpleGraph
    18
    19abbrev Vertex (R : Type*) (c : ℕ) := R × Fin c × Bool
    20
    21def columnGraph (R : Type*) (c : ℕ) : SimpleGraph (Vertex R c) :=
    22 fromRel fun (row, column, side) (row', column', side') =>
    23 (column = column' ∧ side ≠ side') ∨
    24 (row = row' ∧ (column.val + 1 = column'.val ∨ column'.val + 1 = column.val))
    25
    26end Lax762056.ColumnGraph
    27
    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…