Lax Lean Archive

Outerplanar graphs

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

    Outerplanar graph illustration
    Outerplanar graph illustration

    A graph is outerplanar here when it has a crossing-free straight-line drawing with every vertex on one circle, a compact certificate for having every vertex on the boundary of the outer face.

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

    In the paper

    Lean source view on GitHub

    1import Lax68.GraphMinors
    2import Lax68.StraightLineDrawings
    3
    4/-!
    5---
    6title: Outerplanar graphs
    7type: definition
    8---
    9
    10![Outerplanar graph illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/d475531e6ec14f564ed7488033e83d43ae8bd5e6/planar-graph-classes-v4-33/assets/outerplanar.svg "Outerplanar graph illustration")
    11
    12A graph is outerplanar here when it has a crossing-free straight-line drawing
    13with every vertex on one circle, a compact certificate for having every
    14vertex on the boundary of the outer face.
    15-/
    16
    17set_option autoImplicit false
    18
    19namespace Lax68.Outerplanar
    20
    21structure OuterplaneDrawing {V : Type*} (G : SimpleGraph V)
    22 extends StraightLineDrawings.StraightLineDrawing G where
    23 radius : ℝ
    24 radius_pos : 0 < radius
    25 onBoundary :
    26 ∀ v : V,
    27 let p := toStraightLineDrawing.point v
    28 p.1 ^ 2 + p.2 ^ 2 = radius ^ 2
    29
    30def IsOuterplanar {V : Type*} (G : SimpleGraph V) : Prop :=
    31 Nonempty (OuterplaneDrawing G)
    32
    33/-- The usual forbidden-minor characterization of outerplanarity. -/
    34def IsOuterplanarByExcludedMinors {V : Type*} (G : SimpleGraph V) : Prop :=
    35 ¬ GraphMinors.IsMinor GraphMinors.K4 G ∧
    36 ¬ GraphMinors.IsMinor GraphMinors.K23 G
    37
    38end Lax68.Outerplanar
    39
    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…