Lax Lean Archive

Grids and walls

Lax68.GridsAndWalls · concepts/Lax68/GridsAndWalls.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

    Grid and wall illustration
    Grid and wall illustration

    A nonempty rectangular grid has vertices in rows and columns, with edges between orthogonally consecutive positions. A wall is the brick-wall subgraph obtained by retaining alternating vertical grid edges.

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

    In the paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Hasse
    2
    3/-!
    4---
    5title: Grids and walls
    6type: definition
    7---
    8
    9![Grid and wall illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/d0f2a7021b6428f55a4524763f47a4312c74348f/planar-graph-classes-v4-33/assets/grid-wall.svg "Grid and wall illustration")
    10
    11A nonempty rectangular grid has vertices in rows and columns, with edges
    12between orthogonally consecutive positions. A wall is the brick-wall subgraph
    13obtained by retaining alternating vertical grid edges.
    14-/
    15
    16set_option autoImplicit false
    17
    18namespace Lax68.GridsAndWalls
    19
    20def consecutive (a b : ℕ) : Prop :=
    21 a + 1 = b ∨ b + 1 = a
    22
    23def WallAdjacent {m n : ℕ} (u v : Fin m × Fin n) : Prop :=
    24 (u.1 = v.1 ∧ consecutive u.2.val v.2.val) ∨
    25 (u.2 = v.2 ∧
    26 consecutive u.1.val v.1.val ∧
    27 (Nat.min u.1.val v.1.val + u.2.val) % 2 = 0)
    28
    29def HasGridShape {V : Type*} (G : SimpleGraph V) : Prop :=
    30 ∃ m n : ℕ,
    31 0 < m ∧
    32 0 < n ∧
    33 Nonempty
    34 (G ≃g (SimpleGraph.pathGraph m □ SimpleGraph.pathGraph n))
    35
    36def HasWallShape {V : Type*} (G : SimpleGraph V) : Prop :=
    37 ∃ m n : ℕ,
    38 0 < m ∧
    39 0 < n ∧
    40 ∃ e : Fin m × Fin n ≃ V,
    41 ∀ u v,
    42 G.Adj (e u) (e v) ↔ WallAdjacent u v
    43
    44def IsGrid {V : Type*} (G : SimpleGraph V) : Prop :=
    45 HasGridShape G
    46
    47def IsWall {V : Type*} (G : SimpleGraph V) : Prop :=
    48 HasWallShape G
    49
    50end Lax68.GridsAndWalls
    51
    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…