Polygonal paths

A polygonal path is carried by a list of vertices; its poly carrier is the union of the segments joining consecutive entries. This is the combinatorial representation the whole of Part I works with — by the blueprint's polygonal overlay convention only finite polygonal objects are ever overlaid, so vertex lists, not parametrizations, are the primitive.

Blueprint

• poly — the carrier of a polygonal path.
• exists_poly_of_isPreconnected — Lemma 1.1 (polygonal connectedness), less the passage to a simple arc, which needs the finite-graph machinery and is proved with Lemma 1.2.

Segments

theorem Schoenflies.isCompact_segment (x y : Plane) : IsCompact (segment ℝ x y)

The carrier of a vertex list

def Schoenflies.poly : List Plane → Set Plane

The carrier of a polygonal path: the union of the segments joining consecutive vertices. A single vertex carries itself, so that a path may be constant.

Equations

• Schoenflies.poly [] = ∅
• Schoenflies.poly [v] = {v}
• Schoenflies.poly (u :: v :: rest) = segment ℝ u v ∪ Schoenflies.poly (v :: rest)

@[simp]

theorem Schoenflies.poly_nil : poly [] = ∅

@[simp]

theorem Schoenflies.poly_singleton (v : Plane) : poly [v] = {v}

@[simp]

theorem Schoenflies.poly_cons_cons (u v : Plane) (rest : List Plane) : poly (u :: v :: rest) = segment ℝ u v ∪ poly (v :: rest)

theorem Schoenflies.poly_nonempty {vs : List Plane} : vs ≠ [] → (poly vs).Nonempty

theorem Schoenflies.isCompact_poly (vs : List Plane) : IsCompact (poly vs)

theorem Schoenflies.mem_poly_of_mem {vs : List Plane} {v : Plane} : v ∈ vs → v ∈ poly vs

Every vertex lies on the carrier.

theorem Schoenflies.head_mem_poly {vs : List Plane} (h : vs ≠ []) : vs.head h ∈ poly vs

theorem Schoenflies.getLast_mem_poly {vs : List Plane} (h : vs ≠ []) : vs.getLast h ∈ poly vs

theorem Schoenflies.isConnected_poly {vs : List Plane} : vs ≠ [] → IsConnected (poly vs)

The carrier of a nonempty vertex list is connected: consecutive segments share a vertex.

theorem Schoenflies.poly_concat {vs : List Plane} (h : vs ≠ []) (z : Plane) : poly (vs ++ [z]) = poly vs ∪ segment ℝ (vs.getLast h) z

Appending one vertex extends the carrier by one segment.

Polygonal connectedness

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

Lemma 1.1 (polygonal connectedness), existence half. Any two points of a region are joined in it by a polygonal path.

The blueprint goes on to make the path simple, by subdividing at self-intersections and taking a simple path in the resulting finite graph; that half is deferred to the graph module, where the subdivision procedure is available.

theorem Schoenflies.poly_append {vs : List Plane} (h : vs ≠ []) (w : Plane) (rest : List Plane) : vs.getLast h = w → poly (vs ++ w :: rest) = poly vs ∪ poly (w :: rest)

Concatenating two vertex lists that agree at the join concatenates their carriers. The hypothesis is what makes this true: without it poly [a] ∪ poly [b] = {a, b} misses the segment that poly [a, b] carries.