Straight-line planar drawings

DefinitionClosed segment in the plane#✓fully proved

For points \(a\) and \(b\) of \(\mathbb{R}^2\), the closed segment from \(a\) to \(b\) is the set of points \(a + t(b - a)\) with \(t \in \mathbb{R}\) and \(0 \le t \le 1\).

public def Segment (a b : ℝ × ℝ) : Set (ℝ × ℝ) :=
  {p | ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧
    p.1 = a.1 + t * (b.1 - a.1) ∧ p.2 = a.2 + t * (b.2 - a.2)}

Used by 2

Used byStraight-line planar graph · Straight-line planar embedding

DefinitionStraight-line planar graph#✓fully proved

A simple graph \(G\) with vertex set \(V\) is straight-line planar if either \(V\) is empty or there is an injective map \(f\) from \(V\) to \(\mathbb{R}^2\) such that, for any two different edges \(vw\) and \(xy\) of \(G\), the closed segment from \(f(v)\) to \(f(w)\) and the closed segment from \(f(x)\) to \(f(y)\) meet only in points of \(\{f(v), f(w)\} \cap \{f(x), f(y)\}\).

public def IsPlanar {V : Type*} (G : SimpleGraph V) : Prop :=
  ¬Nonempty V ∨
    ∃ f : V → ℝ × ℝ, Function.Injective f ∧
      (∀ ⦃v w⦄, G.Adj v w → f v ≠ f w) ∧
      ∀ ⦃v w x y⦄, G.Adj v w → G.Adj x y →
        ({v, w} : Set V) ≠ {x, y} →
        Segment (f v) (f w) ∩ Segment (f x) (f y) ⊆
          ({f v, f w} : Set (ℝ × ℝ)) ∩ {f x, f y}

Uses 1 · Used by 3

Statement usesClosed segment in the plane

Used byFive color theorem · Prism-Hamiltonicity conjecture for 3-connected planar graphs · Universal point set for planar graphs

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.