Local polygonal connectedness, in the form brick B7 consumes

Schoenflies/LocallyPolygonal.lean (brick B5) and Schoenflies/PolygonalCarrier.lean (brick B6) were written independently and each carries its own "joined by a polygonal path inside a set" relation — PolyConnIn as an existential over vertex lists, PolyReaches as an inductive relation — with its own local form. This module makes them one, and then fixes the shape problem that stops B5 from feeding B7.

The shape problem

Both local forms ask only that the connecting path lie in S:

IsLocallyPolyConnAt S p  :  ∃ U open ∋ p, ∀ x y ∈ U ∩ S, PolyConnIn S x y
IsLocallyPolyConnected C :  ∀ w ∈ C, ∃ V open ∋ w, ∀ z ∈ V ∩ C, PolyReaches C w z

That is enough for B6 — the clopen argument only needs some path — but it is a property with no local content whatsoever: any polygonally connected S satisfies it with U = univ. In particular it does not survive intersection with an open set, and that is exactly what B7 needs: U_e is a component of a relatively open piece of M, and a replacement arc has to stay inside the thin tube, not merely inside M.

The fix is IsLocallyPolyConnAt': arbitrarily small neighbourhoods U of p such that any two points of U ∩ S are joined inside U ∩ S. B5's proof already produces this — its paths are two segments inside convex pieces of the small square about p, and the square's radius may be shrunk freely — so nothing geometric is lost, only misstated. isLocallyPolyConn'_compl_openSquare and isLocallyPolyConn'_compl_biUnion are B5 in the strengthened form, and IsLocallyPolyConn'.weaken recovers the original statements.

Blueprint

Brick B5 ↔ brick B6 of lem:polygonal-redrawing (H6), and the interface B7 uses.

• polyConnIn_iff_polyReaches — the two relations agree.
• IsLocallyPolyConn.isLocallyPolyConnected, IsLocallyPolyConnected.isLocallyPolyConn — the two weak local forms agree, so B5 as originally stated does feed B6.
• IsLocallyPolyConnAt', IsLocallyPolyConn' — the strengthened local form.
• isLocallyPolyConnAt'_of_convex_cover — the strengthened star lemma: a square about p cut by convex pieces, each of which contains p as soon as it is nonempty.
• isLocallyPolyConnAt'_compl_openSquare, isLocallyPolyConn'_compl_biUnion — brick B5, strengthened.
• IsLocallyPolyConn'.inter_isOpen — shrinkability: a relatively open piece of a locally polygonally connected set is locally polygonally connected.
• IsRelOpenIn, isRelOpenIn_connectedComponentIn — components of relatively open subsets are relatively open, the fact B7 quotes for U_e.
• polyReaches_of_isPreconnected_of_isRelOpenIn, polyReaches_connectedComponentIn — the payoff: two points of a connected relatively open piece are joined inside that piece.

The two weak local forms agree

IsLocallyPolyConn quantifies over pairs of points of the neighbourhood, IsLocallyPolyConnected only over paths from the centre; symmetry and transitivity of the relation make the two equivalent.

theorem Schoenflies.IsLocallyPolyConn.isLocallyPolyConnected {S : Set Plane} (h : IsLocallyPolyConn S) : IsLocallyPolyConnected S

Brick B5's conclusion, read as brick B6's hypothesis.

theorem Schoenflies.IsLocallyPolyConnected.isLocallyPolyConn {S : Set Plane} (h : IsLocallyPolyConnected S) : IsLocallyPolyConn S

The converse: a path from the centre to each of two points, run backwards and forwards.

Squares are a neighbourhood basis

B5 builds its neighbourhoods as axis-parallel squares, and the strengthened local form needs them arbitrarily small inside a given open set.

theorem Schoenflies.Plane.openSquare_subset_ball (p : Plane) (ε : ℝ) : p.openSquare (ε / 2) ⊆ Metric.ball p ε

A square of half a radius sits inside the ball of that radius, because √2 < 2. The open counterpart of Plane.closedSquare_subset_ball, restated here so that this module does not have to import the graph layer. No sign condition on the radius: for ε ≤ 0 the square is already empty.

theorem Schoenflies.Plane.exists_openSquare_subset {W : Set Plane} {p : Plane} (hW : IsOpen W) (hp : p ∈ W) {s₀ : ℝ} (hs₀ : 0 < s₀) : ∃ (s : ℝ), 0 < s ∧ s ≤ s₀ ∧ p.openSquare s ⊆ W

Inside any open set around p there is a square about p, of radius at most any prescribed positive bound.

The strengthened local form

def Schoenflies.IsLocallyPolyConnAt' (S : Set Plane) (p : Plane) : Prop

S is polygonally connected near p inside arbitrarily small neighbourhoods: for every open W containing p there is an open U ⊆ W containing p such that any two points of U ∩ S are joined by a polygonal path lying in U ∩ S.

Two strengthenings over IsLocallyPolyConnAt, and both are needed by brick B7. The path is confined to the neighbourhood, not merely to S, because a replacement arc has to stay in its tube; and the neighbourhoods run through a basis at p, because otherwise the property does not survive intersecting S with an open set (IsLocallyPolyConn'.inter_isOpen).

Equations

• One or more equations did not get rendered due to their size.

def Schoenflies.IsLocallyPolyConn' (S : Set Plane) : Prop

S is locally polygonally connected in the strengthened sense.

Equations

• Schoenflies.IsLocallyPolyConn' S = ∀ p ∈ S, Schoenflies.IsLocallyPolyConnAt' S p

theorem Schoenflies.IsLocallyPolyConnAt'.weaken {S : Set Plane} {p : Plane} (h : IsLocallyPolyConnAt' S p) : IsLocallyPolyConnAt S p

theorem Schoenflies.IsLocallyPolyConn'.weaken {S : Set Plane} (h : IsLocallyPolyConn' S) : IsLocallyPolyConn S

The strengthened form implies the original brick B5 statement, so nothing is lost by replacing one with the other.

theorem Schoenflies.IsLocallyPolyConn'.isLocallyPolyConnected {S : Set Plane} (h : IsLocallyPolyConn' S) : IsLocallyPolyConnected S

What brick B6 consumes.

theorem Schoenflies.IsLocallyPolyConnAt'.congr_nhds {S T : Set Plane} {p : Plane} {V : Set Plane} (h : IsLocallyPolyConnAt' T p) (hV : IsOpen V) (hpV : p ∈ V) (heq : S ∩ V = T ∩ V) : IsLocallyPolyConnAt' S p

The property is local: only the trace of S on a neighbourhood of p matters. This is what reduces "finitely many squares" to "one square".

theorem Schoenflies.isLocallyPolyConnAt'_of_nbhd_subset {S : Set Plane} {p : Plane} {V : Set Plane} (hV : IsOpen V) (hpV : p ∈ V) (hVS : V ⊆ S) : IsLocallyPolyConnAt' S p

A neighbourhood of p already inside S settles the point: shrink it to a square, which is convex, so a single segment joins any two of its points.

theorem Schoenflies.isLocallyPolyConn'_of_isOpen {S : Set Plane} (hS : IsOpen S) : IsLocallyPolyConn' S

An open set is locally polygonally connected in the strengthened sense.

theorem Schoenflies.isLocallyPolyConnAt'_of_convex_cover {S : Set Plane} {p : Plane} {ι : Type u_1} {H : ι → Set Plane} {s₀ : ℝ} (hs₀ : 0 < s₀) (hconv : ∀ (i : ι), Convex ℝ (H i)) (hsub : ∀ (i : ι), p.openSquare s₀ ∩ H i ⊆ S) (hcover : p.openSquare s₀ ∩ S ⊆ ⋃ (i : ι), H i) (hstar : ∀ (i : ι), ∀ z ∈ p.openSquare s₀ ∩ H i, p ∈ H i) : IsLocallyPolyConnAt' S p

The strengthened star lemma, and the whole geometric content of brick B5's three shapes. Suppose that inside one square about p the trace of S is covered by convex sets H i, that each H i meets that square only inside S, and that each H i which meets the square contains p. Then S is locally polygonally connected at p in the strengthened sense.

Two points of a small square about p are then joined by two segments through p, each inside one convex piece of that small square — which is why the path never leaves the neighbourhood. No piece is required to be nonempty and none is named, so the disk, the half-disk and the three-quarter disk are all this statement.

Brick B5, strengthened

The two theorems of LocallyPolygonal.lean, reproved in the strengthened form. The geometry is unchanged — Plane.exists_radius_sides still does all the work — because the pieces the old proof used were already inside the neighbourhood; only the statement moves.

theorem Schoenflies.isLocallyPolyConnAt'_compl_openSquare (c : Plane) (r : ℝ) (p : Plane) : IsLocallyPolyConnAt' (c.openSquare r)ᶜ p

The one-square case of brick B5, strengthened. The complement of an open axis-parallel square is polygonally connected near every point of the plane, by paths confined to the neighbourhood.

theorem Schoenflies.isLocallyPolyConn'_compl_biUnion {Q : Set Plane} (hQ : Q.Finite) (ρ : Plane → ℝ) (hdisj : ∀ c ∈ Q, ∀ c' ∈ Q, c ≠ c' → Disjoint (c.closedSquare (ρ c)) (c'.closedSquare (ρ c'))) : IsLocallyPolyConn' (⋃ c ∈ Q, c.openSquare (ρ c))ᶜ

Brick B5, strengthened. The plane minus finitely many open axis-parallel squares whose closed squares are pairwise disjoint is locally polygonally connected, with the connecting paths confined to the neighbourhood.

The two cases are unchanged. Away from all the closed squares a small square about p lies inside M outright. Otherwise p lies in exactly one closed square, and a small enough square about p misses all the others, so near p the set M is the complement of that one open square — which is what IsLocallyPolyConnAt'.congr_nhds says suffices.

Shrinkability

The point of the strengthening. IsLocallyPolyConn does not have this property: it holds for any polygonally connected S with U = univ, and the comb space — the segments {0} × [0,1], {1/n} × [0,1] and [0,1] × {0} — is polygonally connected while its intersection with a thin open strip about y = 1 is not locally polygonally connected at (0,1).

theorem Schoenflies.IsLocallyPolyConnAt'.inter_isOpen {S W : Set Plane} {p : Plane} (h : IsLocallyPolyConnAt' S p) (hW : IsOpen W) (hpW : p ∈ W) : IsLocallyPolyConnAt' (S ∩ W) p

Shrinkability. A relatively open piece of a locally polygonally connected set is locally polygonally connected. Taking the neighbourhood inside W is what makes this work, and it is the reason IsLocallyPolyConnAt' quantifies over all open W ∋ p.

theorem Schoenflies.IsLocallyPolyConn'.inter_isOpen {S W : Set Plane} (h : IsLocallyPolyConn' S) (hW : IsOpen W) : IsLocallyPolyConn' (S ∩ W)

Relatively open subsets and their components

def Schoenflies.IsRelOpenIn (S A : Set Plane) : Prop

A is relatively open in S: cut out of S by an ambient open set.

Equations

• Schoenflies.IsRelOpenIn S A = ∃ (W : Set Schoenflies.Plane), IsOpen W ∧ A = S ∩ W

theorem Schoenflies.IsRelOpenIn.subset {S A : Set Plane} (h : IsRelOpenIn S A) : A ⊆ S

theorem Schoenflies.isRelOpenIn_self (S : Set Plane) : IsRelOpenIn S S

theorem Schoenflies.IsOpen.isRelOpenIn {S A : Set Plane} (hA : IsOpen A) (hAS : A ⊆ S) : IsRelOpenIn S A

theorem Schoenflies.isRelOpenIn_of_exists {S A : Set Plane} (hAS : A ⊆ S) (h : ∃ (U : Set Plane), IsOpen U ∧ A ⊆ U ∧ U ∩ S ⊆ A) : IsRelOpenIn S A

The shape isRelOpen_of_polyReaches_stable delivers, read as relative openness.

theorem Schoenflies.IsRelOpenIn.trans {S A B : Set Plane} (hA : IsRelOpenIn S A) (hB : IsRelOpenIn A B) : IsRelOpenIn S B

Relative openness is transitive, which is how a component of a relatively open piece is seen to be relatively open in the ambient set.

theorem Schoenflies.IsLocallyPolyConn'.of_isRelOpenIn {S A : Set Plane} (h : IsLocallyPolyConn' S) (hA : IsRelOpenIn S A) : IsLocallyPolyConn' A

Shrinkability, phrased for a relatively open piece.

theorem Schoenflies.isRelOpenIn_connectedComponentIn {S A : Set Plane} (h : IsLocallyPolyConn' S) (hA : IsRelOpenIn S A) (x : Plane) : IsRelOpenIn S (connectedComponentIn A x)

Components of relatively open subsets are relatively open. For S locally polygonally connected and A relatively open in S, each connected component of A is relatively open in S.

The proof is isRelOpen_of_polyReaches_stable: a polygonal path inside A is a connected subset of A, so it cannot leave the component it starts in, which is exactly the stability that lemma asks for.

theorem Schoenflies.isLocallyPolyConn'_connectedComponentIn {S A : Set Plane} (h : IsLocallyPolyConn' S) (hA : IsRelOpenIn S A) (x : Plane) : IsLocallyPolyConn' (connectedComponentIn A x)

A component of a relatively open piece is itself locally polygonally connected, so the whole interface applies again one level down.

The payoff

theorem Schoenflies.polyReaches_of_isPreconnected_of_isRelOpenIn {S C : Set Plane} {x y : Plane} (h : IsLocallyPolyConn' S) (hC : IsRelOpenIn S C) (hconn : IsPreconnected C) (hx : x ∈ C) (hy : y ∈ C) : PolyReaches C x y

What brick B7 uses. In a locally polygonally connected S, any two points of a connected relatively open subset are joined by a polygonal path inside that subset.

theorem Schoenflies.exists_poly_of_isPreconnected_of_isRelOpenIn {S C : Set Plane} {x y : Plane} (h : IsLocallyPolyConn' S) (hC : IsRelOpenIn S C) (hconn : IsPreconnected C) (hx : x ∈ C) (hy : y ∈ C) : ∃ (vs : List Plane) (hne : vs ≠ []), poly vs ⊆ C ∧ vs.head hne = x ∧ vs.getLast hne = y

The same, as a vertex list.

theorem Schoenflies.polyReaches_connectedComponentIn {S A : Set Plane} {x y : Plane} (h : IsLocallyPolyConn' S) (hA : IsRelOpenIn S A) {w : Plane} (hx : x ∈ connectedComponentIn A w) (hy : y ∈ connectedComponentIn A w) : PolyReaches (connectedComponentIn A w) x y

The component form, which is how U_e arises: a component of a relatively open piece is both relatively open and polygonally connected in itself.