Simple polygonal arcs

Schoenflies/PolyPath.lean joins two points of a region by a polygonal path — a vertex list whose carrier stays inside the region. A path may cross itself, so it is not an arc. This module supplies the missing half of Lemma 1.1 and, with it, Lemma 1.2, by running the blueprint's recipe: subdivide at all intersections, delete duplicate subsegments, and take a simple path in the resulting finite graph.

The three steps are already available.

• Subdividing and deduplicating is Schoenflies.overlayGraph: a finite list of nondegenerate segments becomes a finite plane graph whose point set is exactly their union (Schoenflies.overlayGraph_pointSet).
• A simple path in that graph is Graph.IsPath, produced by Graph.Reaches.exists_isPath.
• Its realisation is an arc between its ends, by Graph.IsDrawing.path_isArcBetween.

What actually has to be proved here

Two things, and neither is in the list above.

The graph is connected when the union is. The overlay is built from geometry, so nothing so far says that two points joined in the plane are joined along edges. The argument is a clopen one: for a vertex a, the points carried by the edges the walk relation can reach from a form a compact set, the points carried by the other edges form another, the two are disjoint — a common point would be a vertex incident with edges from both classes, by the drawing condition — and together they are the whole union. Preconnectedness then forces the second class to carry nothing.

The realisation of a path is poly of a vertex list. Graph.IsDrawing.path_isArcBetween delivers Graph.edgesCover, a union of edge arcs with no order in it, while IsPolygonal and every polygonal consumer downstream want a vertex list. Schoenflies.exists_poly_eq_edgesCover recovers one by induction along the walk. Its statement returns the list, not the bare existence of some polygonal set, so a consumer that needs the vertices — the redrawing argument does — still has them.

Both endpoints have to be vertices of the overlay, which is arranged by putting them on the list of cut points: EndsAreCut and MeetsAreCut only ask that certain points occur in that list, so lengthening it is free.

Blueprint

• Schoenflies.segsOf, Schoenflies.cover_segsOf — a vertex list read as a list of nondegenerate segments, the input format the overlay wants.
• Schoenflies.overlayGraph_reaches — the overlay graph of a connected union is connected.
• Schoenflies.exists_simple_poly_of_cover — Lemma 1.2 (finite polygonal unions), for a union given as a finite list of nondegenerate segments.
• Schoenflies.exists_simple_poly_of_poly, Schoenflies.exists_simple_poly_of_isPolygonal — Lemma 1.2 for a set presented as a polygonal carrier.
• Schoenflies.exists_simple_poly_of_biUnion, Schoenflies.exists_simple_poly_of_union — Lemma 1.2 as the blueprint states it, for a finite union of polygonal sets.
• Schoenflies.exists_simple_poly_of_isPreconnected, Schoenflies.exists_simple_arc_of_isPreconnected — Lemma 1.1 (polygonal connectedness), in full: any two points of a region are joined in it by a simple polygonal arc.

Two lemmas that belong elsewhere

Schoenflies.cover_flatMap_list generalises Schoenflies.cover_flatMap to an arbitrary index list and belongs beside it in Schoenflies/Subdivide.lean; Schoenflies.subset_of_finite_diff is a general fact about preconnected sets. Both are here only because their homes are on main.

One more shape of poly

poly_cons_cons peels a segment off a list of length at least two. The overlay's induction peels one off a list known only to be nonempty, so it needs the head as a term rather than as a pattern.

theorem Schoenflies.poly_cons_of_ne_nil {vs : List Plane} (h : vs ≠ []) (u : Plane) : poly (u :: vs) = segment ℝ u (vs.head h) ∪ poly vs

Prepending a vertex to a nonempty list adds the segment to its head.

The segments of a vertex list

poly is a chain: consecutive vertices, with repetitions allowed. The overlay takes a list of pieces and insists that each be nondegenerate, so a repetition has to be dropped rather than passed on. Dropping one is harmless — a degenerate segment is a single point, and that point is an end of the neighbouring segment — except when the whole chain degenerates to a point, which is the second disjunct of cover_segsOf.

noncomputable def Schoenflies.segsOf : List Plane → List Piece

The nondegenerate segments of a polygonal chain, in order. A repeated vertex contributes nothing.

Equations

• Schoenflies.segsOf [] = []
• Schoenflies.segsOf [head] = []
• Schoenflies.segsOf (u :: v :: rest) = if u = v then Schoenflies.segsOf (v :: rest) else (u, v) :: Schoenflies.segsOf (v :: rest)

@[simp]

theorem Schoenflies.segsOf_nil : segsOf [] = []

@[simp]

theorem Schoenflies.segsOf_singleton (v : Plane) : segsOf [v] = []

theorem Schoenflies.segsOf_cons_cons (u v : Plane) (rest : List Plane) : segsOf (u :: v :: rest) = if u = v then segsOf (v :: rest) else (u, v) :: segsOf (v :: rest)

theorem Schoenflies.segsOf_nondeg (vs : List Plane) (P : Piece) : P ∈ segsOf vs → P.Nondeg

Every segment produced is nondegenerate — which is the whole point of the definition.

theorem Schoenflies.cover_segsOf (vs : List Plane) : cover (segsOf vs) = poly vs ∨ segsOf vs = [] ∧ (poly vs).Subsingleton

The segments of a chain occupy the chain — unless the chain has collapsed to a point (or to nothing), in which case there are no segments at all.

theorem Schoenflies.cover_segsOf_eq {a b : Plane} {vs : List Plane} (ha : a ∈ poly vs) (hb : b ∈ poly vs) (hab : a ≠ b) : cover (segsOf vs) = poly vs

When a chain carries two distinct points it has not collapsed, so its segments occupy exactly it.

The realisation of a walk is a polygonal chain

Graph.edgesCover is a union with no order in it. The walk supplies the order, and the induction reads the vertex list off it.

theorem Schoenflies.exists_poly_eq_edgesCover {pieces : List Piece} {points : List Plane} {u v : Plane} {W : List Piece} (hW : (overlayGraph pieces points).IsWalk u W v) (hne : W ≠ []) : ∃ (vs : List Plane) (h : vs ≠ []), vs.head h = u ∧ vs.getLast h = v ∧ poly vs = Graph.edgesCover segmentDrawing W

The realisation of a nonempty walk of the overlay graph is the carrier of a vertex list, running from the walk's source to its target.

The list is returned rather than an unnamed polygonal set: the consumers of Lemma 1.1 that overlay the arc with something else need its vertices.

The overlay graph of a connected union is connected

Nothing built so far relates the plane topology of the union to the walk relation of the graph. This is where they meet.

theorem Schoenflies.overlayGraph_reaches_end {pieces : List Piece} {points : List Plane} {a x : Plane} {P : Piece} (hP : P ∈ overlayPieces pieces points) (hz : x = P.1 ∨ x = P.2) : (overlayGraph pieces points).Reaches a P.1 ↔ (overlayGraph pieces points).Reaches a x

Both ends of an edge reach the same vertices.

theorem Schoenflies.overlayGraph_mem_vertexSet_of_mem_cover {pieces : List Piece} {points : List Plane} {x : Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hxp : x ∈ points) (hx : x ∈ cover pieces) : x ∈ (overlayGraph pieces points).vertexSet

A cut point on the union is a vertex: it lies on some edge, and a cut point is interior to no edge, so it is one of that edge's two ends.

theorem Schoenflies.overlayGraph_reaches {pieces : List Piece} {points : List Plane} {a b : Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hconn : IsPreconnected (cover pieces)) (hEnds : EndsAreCut pieces points) (hMeets : MeetsAreCut pieces points) (hap : a ∈ points) (hbp : b ∈ points) (ha : a ∈ cover pieces) (hb : b ∈ cover pieces) : (overlayGraph pieces points).Reaches a b

The overlay graph of a connected union is connected, in the form the construction needs: any vertex reaches any other.

The proof is a clopen argument in the plane. Split the edges into those whose ends the walk relation reaches from a and those it does not; each class carries a compact set, the two carried sets cover the union, and they are disjoint — a common point would, by the drawing condition, be a vertex incident with an edge of each class, and incidence is reachability. Preconnectedness then leaves the second class carrying nothing.

Lemma 1.2, and then Lemma 1.1

theorem Schoenflies.exists_simple_poly_of_cover {pieces : List Piece} {a b : Plane} (hnd : ∀ P ∈ pieces, P.Nondeg) (hconn : IsPreconnected (cover pieces)) (hab : a ≠ b) (ha : a ∈ cover pieces) (hb : b ∈ cover pieces) : ∃ (vs : List Plane) (h : vs ≠ []), vs.head h = a ∧ vs.getLast h = b ∧ poly vs ⊆ cover pieces ∧ IsArcBetween (poly vs) a b

Lemma 1.2 (finite polygonal unions). If a finite union of nondegenerate segments is connected, any two distinct points of it are joined inside it by a simple polygonal arc.

The arc is returned as a vertex list, not merely as a set: the consumers that overlay it with another polygonal object need its vertices, and an existential over sets would not give them back.

theorem Schoenflies.exists_simple_poly_of_poly {a b : Plane} {vs : List Plane} (hconn : IsPreconnected (poly vs)) (hab : a ≠ b) (ha : a ∈ poly vs) (hb : b ∈ poly vs) : ∃ (ws : List Plane) (h : ws ≠ []), ws.head h = a ∧ ws.getLast h = b ∧ poly ws ⊆ poly vs ∧ IsArcBetween (poly ws) a b

Lemma 1.2, for a set presented as a polygonal chain.

theorem Schoenflies.exists_simple_poly_of_isPolygonal {a b : Plane} {A : Set Plane} (hA : IsPolygonal A) (hconn : IsPreconnected A) (hab : a ≠ b) (ha : a ∈ A) (hb : b ∈ A) : ∃ (ws : List Plane) (h : ws ≠ []), ws.head h = a ∧ ws.getLast h = b ∧ poly ws ⊆ A ∧ IsArcBetween (poly ws) a b

Lemma 1.2, for a set given only as polygonal.

A finite union of polygonal arcs

The blueprint states Lemma 1.2 for a finite union, which Schoenflies.cover already is. The only thing standing between the two readings is that a member of the union may have collapsed to a single point, contributing no segment at all. A collapsed member is harmless: were its point missing from the segments, it would be clopen in the union, which a connected set with more than one point does not tolerate.

theorem Schoenflies.biUnion_list_cons {α : Type u_1} (f : α → Set Plane) (x : α) (l : List α) : ⋃ y ∈ x :: l, f y = f x ∪ ⋃ y ∈ l, f y

Peeling the head off a union indexed by a list.

theorem Schoenflies.cover_flatMap_list {α : Type u_1} (f : α → List Piece) (l : List α) : cover (List.flatMap f l) = ⋃ x ∈ l, cover (f x)

Schoenflies.cover_flatMap, over an arbitrary index list rather than a list of pieces. Belongs beside it in Schoenflies/Subdivide.lean; it is here because that module is on main.

theorem Schoenflies.subset_of_finite_diff {a b : Plane} {U C : Set Plane} (hU : IsPreconnected U) (hC : IsClosed C) (hfin : (U \ C).Finite) (ha : a ∈ U) (hb : b ∈ U) (hab : a ≠ b) : U ⊆ C

A preconnected set with two distinct points absorbs finitely many stray points: it cannot be a closed set together with finitely many extra points, since each extra point would be clopen in it.

theorem Schoenflies.exists_simple_poly_of_biUnion {a b : Plane} {L : List (List Plane)} (hconn : IsPreconnected (⋃ vs ∈ L, poly vs)) (hab : a ≠ b) (ha : a ∈ ⋃ vs ∈ L, poly vs) (hb : b ∈ ⋃ vs ∈ L, poly vs) : ∃ (ws : List Plane) (h : ws ≠ []), ws.head h = a ∧ ws.getLast h = b ∧ poly ws ⊆ ⋃ vs ∈ L, poly vs ∧ IsArcBetween (poly ws) a b

Lemma 1.2 (finite polygonal unions). A connected finite union of polygonal chains joins any two of its distinct points by a simple polygonal arc inside it.

theorem Schoenflies.exists_lists_of_isPolygonal {L : List (Set Plane)} : (∀ A ∈ L, IsPolygonal A) → ∃ (M : List (List Plane)), ⋃ vs ∈ M, poly vs = ⋃ A ∈ L, A

A list of polygonal sets is a list of polygonal chains.

theorem Schoenflies.exists_simple_poly_of_union {a b : Plane} {L : List (Set Plane)} (hL : ∀ A ∈ L, IsPolygonal A) (hconn : IsPreconnected (⋃ A ∈ L, A)) (hab : a ≠ b) (ha : a ∈ ⋃ A ∈ L, A) (hb : b ∈ ⋃ A ∈ L, A) : ∃ (ws : List Plane) (h : ws ≠ []), ws.head h = a ∧ ws.getLast h = b ∧ poly ws ⊆ ⋃ A ∈ L, A ∧ IsArcBetween (poly ws) a b

Lemma 1.2 (finite polygonal unions), at the level of sets: if a connected set is the union of finitely many polygonal sets, any two of its distinct points are joined in it by a simple polygonal arc.

theorem Schoenflies.exists_simple_poly_of_isPreconnected {Ω : Set Plane} {x y : Plane} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hx : x ∈ Ω) (hy : y ∈ Ω) (hxy : x ≠ y) : ∃ (vs : List Plane) (h : vs ≠ []), vs.head h = x ∧ vs.getLast h = y ∧ poly vs ⊆ Ω ∧ IsArcBetween (poly vs) x y

Lemma 1.1 (polygonal connectedness), in full. Any two distinct points of a region are joined in it by a simple polygonal arc.

Schoenflies.exists_poly_of_isPreconnected supplies a polygonal path; Lemma 1.2 extracts a simple arc from its carrier.

theorem Schoenflies.exists_simple_arc_of_isPreconnected {Ω : Set Plane} {x y : Plane} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hx : x ∈ Ω) (hy : y ∈ Ω) (hxy : x ≠ y) : ∃ A ⊆ Ω, IsPolygonal A ∧ IsArcBetween A x y

Lemma 1.1, in set form: a simple polygonal arc inside the region between any two of its points.