Polygonal sets, and segments as arcs

IsPolygonal is the blueprint's set-level predicate: a finite union of line segments, which here is exactly the carrier of some vertex list.

The theorem the plane-graph layer needs from this module is isArcBetween_segment: a nondegenerate segment is an arc between its endpoints. It is what makes the drawing condition free for a polygonal plane graph — an edge's arc obligation is discharged by the segment itself, and the distinctness of its ends is already part of well-formedness.

Blueprint

• IsPolygonal — §1, "an arc or curve is polygonal if it is a finite union of line segments".
• isArcBetween_segment — a nondegenerate segment is an arc between its endpoints.

def Schoenflies.IsPolygonal (A : Set Plane) : Prop

A set is polygonal when it is the carrier of a finite vertex list, that is, a finite union of line segments.

Equations

• Schoenflies.IsPolygonal A = ∃ (vs : List Schoenflies.Plane), A = Schoenflies.poly vs

theorem Schoenflies.IsPolygonal.isCompact {A : Set Plane} (h : IsPolygonal A) : IsCompact A

theorem Schoenflies.poly_pair (a b : Plane) : poly [a, b] = segment ℝ a b

theorem Schoenflies.isPolygonal_segment (a b : Plane) : IsPolygonal (segment ℝ a b)

theorem Schoenflies.injOn_lineMap {I : Set ℝ} {a b : Plane} (hab : a ≠ b) : Set.InjOn (⇑(AffineMap.lineMap a b)) I

lineMap a b is injective on the unit interval exactly when the segment is nondegenerate: two parameters differ by a multiple of b - a. Exposed separately because the plane-graph drawing condition asks for the parametrization, not just its image.

theorem Schoenflies.isArcBetween_segment {a b : Plane} (hab : a ≠ b) : IsArcBetween (segment ℝ a b) a b

A nondegenerate segment is an arc between its endpoints, parametrized by AffineMap.lineMap a b.

theorem Schoenflies.isArc_segment {a b : Plane} (hab : a ≠ b) : IsArc (segment ℝ a b)

theorem Schoenflies.exists_poly_anchored (vs : List Plane) : vs ≠ [] → ∀ (z w : Plane), z ∈ poly vs → w ∈ poly vs → ∃ (mid : List Plane), poly (z :: (mid ++ [w])) = poly vs

A polygonal set is carried by a vertex list running from any of its points to any other. The list is written with its two ends displayed, so no List.head/List.getLast obligations appear.

theorem Schoenflies.IsPolygonal.union {A B : Set Plane} (hA : IsPolygonal A) (hB : IsPolygonal B) (hmeet : (A ∩ B).Nonempty) : IsPolygonal (A ∪ B)

Two polygonal sets that meet have a polygonal union. Anchor both lists at a common point and concatenate.