Polygonal connectedness over a carrier

Schoenflies.exists_poly_of_isPreconnected joins two points of an open connected subset of the plane by a polygonal path. The redrawing argument needs the same conclusion for a carrier that is not open in the plane: the ambient set there is the plane minus finitely many open squares, and the basic neighbourhood of a point on a square's boundary is a half-disk or a three-quarter disk rather than a ball.

This module restates the clopen argument over an arbitrary carrier C. The only hypothesis on C is that it is locally polygonally connected: every point has a relatively open neighbourhood all of whose points it reaches by a polygonal path inside C. Openness of C is used nowhere; the ball of the classical proof appears only in isLocallyPolyConnected_of_isOpen, which is what recovers the old statement.

Blueprint

Brick B6 of lem:polygonal-redrawing (H6): polygonal connectivity one level up.

• PolyReaches — "joined by a polygonal path inside C", as an inductive relation. LocallyPolygonal.lean exposes its vertex-list representation and delegates the relation operations to this implementation.
• IsLocallyPolyConnected — the hypothesis replacing openness.
• PolyReaches.of_isPreconnected — Lemma 1.1 (polygonal connectedness) over a carrier.
• exists_poly_of_isPreconnected' — the old exists_poly_of_isPreconnected re-derived from it, verbatim; the example below it is a machine check that the statements agree.

Joined by a polygonal path inside a carrier

inductive Schoenflies.PolyReaches (C : Set Plane) (x : Plane) : Plane → Prop

PolyReaches C x y: there is a polygonal path from x to y all of whose segments lie in C. Built at the far end — a path is extended by one segment at a time — because that is the shape both halves of the clopen argument use. refl carries x ∈ C so that a constant path witnesses membership, matching poly [x] = {x}.

• refl {C : Set Plane} {x : Plane} (hx : x ∈ C) : PolyReaches C x x
• step {C : Set Plane} {x y z : Plane} (h : PolyReaches C x y) (hseg : segment ℝ y z ⊆ C) : PolyReaches C x z

theorem Schoenflies.PolyReaches.of_segment {C : Set Plane} {x y : Plane} (hseg : segment ℝ x y ⊆ C) : PolyReaches C x y

A single segment inside C is already a polygonal path.

theorem Schoenflies.PolyReaches.left_mem {C : Set Plane} {x y : Plane} (h : PolyReaches C x y) : x ∈ C

theorem Schoenflies.PolyReaches.right_mem {C : Set Plane} {x y : Plane} (h : PolyReaches C x y) : y ∈ C

theorem Schoenflies.PolyReaches.trans {C : Set Plane} {x y z : Plane} (h₁ : PolyReaches C x y) (h₂ : PolyReaches C y z) : PolyReaches C x z

theorem Schoenflies.PolyReaches.symm {C : Set Plane} {x y : Plane} (h : PolyReaches C x y) : PolyReaches C y x

Symmetry: a path is run backwards one segment at a time, each reversed segment being the same set.

theorem Schoenflies.PolyReaches.mono {C D : Set Plane} {x y : Plane} (hCD : C ⊆ D) (h : PolyReaches C x y) : PolyReaches D x y

The relation and the vertex-list representation agree

theorem Schoenflies.PolyReaches.exists_poly {C : Set Plane} {x y : Plane} (h : PolyReaches C x y) : ∃ (vs : List Plane) (hne : vs ≠ []), poly vs ⊆ C ∧ vs.head hne = x ∧ vs.getLast hne = y

A polygonal path in the sense of PolyReaches yields a vertex list with the carrier of its polygon inside C. This is poly_concat used once per step.

theorem Schoenflies.polyReaches_of_poly_subset {C : Set Plane} {vs : List Plane} (hne : vs ≠ []) : poly vs ⊆ C → PolyReaches C (vs.head hne) (vs.getLast hne)

Conversely a vertex list whose polygon lies in C joins its ends.

Local polygonal connectedness

def Schoenflies.IsLocallyPolyConnected (C : Set Plane) : Prop

C is locally polygonally connected when every point of C has a relatively open neighbourhood in C each of whose points it reaches by a polygonal path inside C.

The neighbourhood is presented as V ∩ C for an ambient open V, which is exactly what a relatively open neighbourhood is; the paths are only required to stay inside C, not inside the neighbourhood, since that is all the clopen argument uses and it is the weaker demand on a producer. Ball, half-disk and three-quarter disk all qualify.

Equations

• Schoenflies.IsLocallyPolyConnected C = ∀ w ∈ C, ∃ (V : Set Schoenflies.Plane), IsOpen V ∧ w ∈ V ∧ ∀ z ∈ V ∩ C, Schoenflies.PolyReaches C w z

theorem Schoenflies.isRelOpen_of_polyReaches_stable {C : Set Plane} (hloc : IsLocallyPolyConnected C) {S : Set Plane} (hS : S ⊆ C) (hstable : ∀ w ∈ S, ∀ z ∈ C, PolyReaches C w z → z ∈ S) : ∃ (U : Set Plane), IsOpen U ∧ S ⊆ U ∧ U ∩ C ⊆ S

The relative-openness step, stated once because the clopen argument uses it twice — for the reachable set and, run backwards, for its relative complement.

A subset of C closed under "reach one more point of C by a polygonal path" is relatively open in C. The witness is the union of all ambient open sets that are polygonally attached to a point of S; no choice is needed to assemble it.

The theorem

theorem Schoenflies.PolyReaches.of_isPreconnected {C : Set Plane} {x y : Plane} (hloc : IsLocallyPolyConnected C) (hconn : IsPreconnected C) (hx : x ∈ C) (hy : y ∈ C) : PolyReaches C x y

Lemma 1.1 (polygonal connectedness) over a carrier: in a relatively connected, locally polygonally connected set, any two points are joined by a polygonal path inside the set.

The proof is the clopen argument. The points reachable from x are relatively open in C, and so are the unreachable ones — the same lemma, since "unreachable" is stable under reaching too, by symmetry. IsPreconnected C then forbids the split.

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

The vertex-list reading of the carrier theorem, matching the shape PolyPath delivers.

Producers of the hypothesis

theorem Schoenflies.polyReaches_union_of_convex {C : Set Plane} {x y : Plane} {S T : Set Plane} (hS : Convex ℝ S) (hT : Convex ℝ T) (hST : (S ∩ T).Nonempty) (hsub : S ∪ T ⊆ C) (hx : x ∈ S ∪ T) (hy : y ∈ S ∪ T) : PolyReaches C x y

Two convex pieces of C that meet make one polygonally connected piece: the bent path through a common point. This is the shape brick B5 needs for the corner neighbourhood, which is a disk minus an open quadrant — the union of two half-disks.

theorem Schoenflies.isLocallyPolyConnected_of_isOpen {C : Set Plane} (hC : IsOpen C) : IsLocallyPolyConnected C

An open set is locally polygonally connected: the balls it contains are convex. This is the only place a ball appears, and it is what recovers the old statement.

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

PolyPath.exists_poly_of_isPreconnected, re-derived from the carrier version.