Lax Lean Archive

Maximal outerplanar graphs

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

    Maximal outerplanar illustration
    Maximal outerplanar illustration

    An outerplanar graph is maximal outerplanar when no edge can be added between its existing vertices while preserving outerplanarity.

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

    In the paper

    Lean source view on GitHub

    1import Lax68.Outerplanar
    2
    3/-!
    4---
    5title: Maximal outerplanar graphs
    6type: definition
    7---
    8
    9![Maximal outerplanar illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/4dd917c8b9a1e181ec951b7f6fa384262af31fa9/planar-graph-classes-v4-33/assets/maximal-outerplanar.svg "Maximal outerplanar illustration")
    10
    11An outerplanar graph is maximal outerplanar when no edge can be added between
    12its existing vertices while preserving outerplanarity.
    13-/
    14
    15set_option autoImplicit false
    16
    17namespace Lax68.MaximalOuterplanar
    18
    19def IsMaximalOuterplanar {V : Type*}
    20 (G : SimpleGraph V) : Prop :=
    21 Outerplanar.IsOuterplanar G ∧
    22 ∀ H : SimpleGraph V,
    23 G < H →
    24 ¬ Outerplanar.IsOuterplanar H
    25
    26end Lax68.MaximalOuterplanar
    27
    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…