Lax Lean Archive

Asteroidal cycle triples obstruct induced minors

Lax222097.CycleObstruction · concepts/Lax222097/CycleObstruction.lean · lax-222097

proven

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

    Lemma

    No graph containing an asteroidal triple of cycles is an induced minor of a row and column graph. The 5×55\times5 grid contains such a triple.

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 asteroidalCycles_obstruction proven

    2 grid_five_has_asteroidalCycles proven

    In the paper

    • page 5 of this submission's paper
    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Lax222097.AsteroidalCycles
    2import Lax222097.ColumnGraph
    3import Lax222097.Grid
    4
    5/-!
    6---
    7title: Asteroidal cycle triples obstruct induced minors
    8type: lemma
    9---
    10No graph containing an asteroidal triple of cycles is an induced minor of
    11a row and column graph. The 5×55\times5 grid contains such a triple.
    12-/
    13
    14namespace Lax222097.CycleObstruction
    15
    16open AsteroidalCycles ColumnGraph Grid InducedMinors
    17
    18axiom asteroidalCycles_obstruction (R W : Type*) (c : ℕ) (H : SimpleGraph W)
    19 (hH : HasAsteroidalCycleTriple H) :
    20 ¬ IsInducedMinor H (columnGraph R c)
    21
    22axiom grid_five_has_asteroidalCycles : HasAsteroidalCycleTriple (squareGrid 5)
    23
    24end Lax222097.CycleObstruction
    25
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…