Lax Lean Archive

Straight-line graph drawings

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

    Straight-line drawing illustration
    Straight-line drawing illustration

    A straight-line drawing assigns distinct points of the real plane to the vertices of a simple graph and draws every edge as the segment between its endpoints. No vertex lies inside an edge and disjoint edges do not meet. This is the geometric drawing certificate used by the planar-graph concept.

    Concept map
    1 concept
    100%
    DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Analysis.Convex.Segment
    2import Mathlib.Combinatorics.SimpleGraph.Basic
    3import Mathlib.Data.Real.Basic
    4
    5/-!
    6---
    7title: Straight-line graph drawings
    8type: definition
    9---
    10
    11![Straight-line drawing illustration](https://raw.githubusercontent.com/lax-archive/lax-submissions/56a5a1328deb64eaacc857b9cb6f53fc0b0b3461/planar-graph-classes-v4-33/assets/straight-line-drawing.svg "Straight-line drawing illustration")
    12
    13A straight-line drawing assigns distinct points of the real plane to the
    14vertices of a simple graph and draws every edge as the segment between its
    15endpoints. No vertex lies inside an edge and disjoint edges do not meet.
    16This is the geometric drawing certificate used by the planar-graph concept.
    17-/
    18
    19set_option autoImplicit false
    20
    21namespace Lax68.StraightLineDrawings
    22
    23abbrev Point := ℝ × ℝ
    24
    25structure StraightLineDrawing {V : Type*} (G : SimpleGraph V) where
    26 point : V → Point
    27 injective : Function.Injective point
    28 noVertexOnEdge :
    29 ∀ {a b c : V},
    30 G.Adj a b →
    31 c ≠ a →
    32 c ≠ b →
    33 point c ∉ segment ℝ (point a) (point b)
    34 disjointEdges :
    35 ∀ {a b c d : V},
    36 G.Adj a b →
    37 G.Adj c d →
    38 Disjoint ({a, b} : Set V) ({c, d} : Set V) →
    39 Disjoint
    40 (segment ℝ (point a) (point b))
    41 (segment ℝ (point c) (point d))
    42
    43def HasStraightLineDrawing {V : Type*} (G : SimpleGraph V) : Prop :=
    44 Nonempty (StraightLineDrawing G)
    45
    46end Lax68.StraightLineDrawings
    47
    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…