Lax Lean Archive

Planar graphs

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

    Planar graph illustration
    Planar graph illustration

    A graph is planar here when it has a crossing-free straight-line drawing in the real plane. For finite simple graphs, this agrees with the usual notion of planarity. The drawing certificate is supplied by a separate concept.

    Concept map
    3 concepts
    100%
    DefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    In the paper

    Lean source view on GitHub

    1import Lax68.GraphMinors
    2import Lax68.StraightLineDrawings
    3
    4/-!
    5---
    6title: Planar graphs
    7type: definition
    8---
    9
    10![Planar graph illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/1d7f2bc99763b554a5d59824c6c0d682f8241254/planar-graph-classes-v4-33/assets/planar.svg "Planar graph illustration")
    11
    12A graph is planar here when it has a crossing-free straight-line drawing in
    13the real plane. For finite simple graphs, this agrees with the usual notion
    14of planarity. The drawing certificate is supplied by a separate concept.
    15-/
    16
    17set_option autoImplicit false
    18
    19namespace Lax68.Planar
    20
    21/-- Existence of a crossing-free straight-line drawing in the real plane. -/
    22def IsPlanar {V : Type*} (G : SimpleGraph V) : Prop :=
    23 StraightLineDrawings.HasStraightLineDrawing G
    24
    25def IsPlanarByExcludedMinors {V : Type*} (G : SimpleGraph V) : Prop :=
    26 ¬GraphMinors.IsMinor GraphMinors.K5 G ∧
    27 ¬GraphMinors.IsMinor GraphMinors.K33 G
    28
    29end Lax68.Planar
    30
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…