Lax Lean Archive

Ladders

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

    Ladder graph illustration
    Ladder graph illustration

    A finite ladder is a nonempty two-row grid: two paths joined by corresponding rungs.

    Concept map
    1 concept; 2 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: Ladders
    6type: definition
    7---
    8
    9![Ladder graph illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/4dd917c8b9a1e181ec951b7f6fa384262af31fa9/planar-graph-classes-v4-33/assets/ladder.svg "Ladder graph illustration")
    10
    11A finite ladder is a nonempty two-row grid: two paths joined by corresponding
    12rungs.
    13-/
    14
    15set_option autoImplicit false
    16
    17namespace Lax68.Ladders
    18
    19def HasLadderShape {V : Type*} (G : SimpleGraph V) : Prop :=
    20 ∃ n : ℕ,
    21 0 < n ∧
    22 Nonempty
    23 (G ≃g (SimpleGraph.pathGraph n □ SimpleGraph.pathGraph 2))
    24
    25def IsLadder {V : Type*} (G : SimpleGraph V) : Prop :=
    26 HasLadderShape G
    27
    28end Lax68.Ladders
    29
    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…