definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
The square grid of order has vertex set . Two vertices are adjacent when they agree in one coordinate and are consecutive in the other.
The definition is the Cartesian box product of two copies of mathlib's finite path graph. Thus order zero gives the empty graph and order one gives a single isolated vertex.
Lean source view on GitHub
| 1 | import Mathlib.Combinatorics.SimpleGraph.Hasse |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Prod |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Square grid graphs |
| 7 | type: definition |
| 8 | --- |
| 9 | The square grid of order \(g\) has vertex set |
| 10 | \(\{0,\ldots,g-1\}\times\{0,\ldots,g-1\}\). Two vertices are adjacent when |
| 11 | they agree in one coordinate and are consecutive in the other. |
| 12 | |
| 13 | The definition is the Cartesian box product of two copies of mathlib's |
| 14 | finite path graph. Thus order zero gives the empty graph and order one gives |
| 15 | a single isolated vertex. |
| 16 | -/ |
| 17 | |
| 18 | namespace Lax17.Grid |
| 19 | |
| 20 | /-- The canonical `g × g` square grid. -/ |
| 21 | def squareGrid (g : ℕ) : SimpleGraph (Fin g × Fin g) := |
| 22 | SimpleGraph.pathGraph g □ SimpleGraph.pathGraph g |
| 23 | |
| 24 | end Lax17.Grid |
| 25 |
Builds on
none
Used by
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