Lax Lean Archive

Excluded induced grid minors

Lax762056.Grid · concepts/Lax762056/Grid.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

    The k×kk\times k square grid is the Cartesian product of two kk-vertex paths. A graph excludes the induced grid of size kk if this square grid is not an induced minor of the graph.

    Concept map
    2 concepts; 4 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Hasse
    2import Lax762056.InducedMinors
    3
    4/-!
    5---
    6title: Excluded induced grid minors
    7type: definition
    8---
    9The k×kk\times k square grid is the Cartesian product of two kk-vertex paths.
    10A graph excludes the induced grid of size kk if this square grid is not
    11an induced minor of the graph.
    12-/
    13
    14namespace Lax762056.Grid
    15
    16open SimpleGraph InducedMinors
    17
    18def squareGrid (k : ℕ) : SimpleGraph (Fin k × Fin k) :=
    19 (pathGraph k).boxProd (pathGraph k)
    20
    21def ExcludesInducedGrid (k : ℕ) {V : Type*} (G : SimpleGraph V) : Prop :=
    22 ¬ IsInducedMinor (squareGrid k) G
    23
    24end Lax762056.Grid
    25
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…