The plane minus finitely many open squares is locally polygonally connected

This is brick B5 of the polygonal-redrawing argument. The redrawing cuts an open axis-parallel square out of the plane around each vertex of the graph; what the rest of the argument needs of the leftover set M is that it is locally polygonally connected — every point of M has a relatively open neighbourhood all of whose points are joined to each other by polygonal paths running inside M. That is what feeds the clopen argument one level up (brick B6), where the basic open piece is no longer a ball.

The informal description of the three basic shapes — a disk away from every square, a half-disk against one side, a three-quarter disk at a corner — suggests an angular case analysis. There is none here. Both the squares and the basic neighbourhoods are axis-parallel, so each shape is an intersection of a small square with the complement of an open square, and

• the complement of an open square is the union of the four closed coordinate half-planes that bound it (Plane.compl_openSquare_subset_iUnion);
• intersecting with a small square gives four rectangles, each convex;
• if the small square is small enough, each of those rectangles is either empty or contains the centre p (Plane.exists_radius_sides).

A union of convex sets with a common point is polygonally connected by two segments through that point, which is isLocallyPolyConnAt_of_star. The three shapes are then just the three ways the list of nonempty pieces can come out (one, two adjacent, or two adjacent again with p on the corner) and none of them has to be named.

The passage from one square to finitely many is a shrinking step: since the closed squares are pairwise disjoint, a point lies in at most one of them, and a small enough neighbourhood of any point misses all the others outright, so M looks locally exactly like the one-square case.

Blueprint

• PolyConnIn — "joined by a polygonal path inside S"; the relation Lemma 1.1 produces.
• IsLocallyPolyConn — the local form of polygonal connectedness, brick B5's conclusion.
• polyConnIn_of_convex, polyConnIn_union_of_convex — a rectangle, and two rectangles that meet, are polygonally connected.
• Plane.sideHalfPlane, Plane.sideGap — the four half-planes bounding a square and the room between a point and each of them.
• isLocallyPolyConnAt_compl_openSquare — the one-square case: the complement of any open square is locally polygonally connected, at every point of the plane.
• isLocallyPolyConn_compl_biUnion — brick B5: the plane minus finitely many open squares with pairwise disjoint closures is locally polygonally connected.

Two list lemmas about poly

PolyPath.lean has poly_concat, which extends a vertex list by a single vertex. Transitivity and symmetry of polygonal connectedness need the two-list versions; both are general facts about poly and belong beside poly_concat rather than here.

theorem Schoenflies.poly_reverse (vs : List Plane) : poly vs.reverse = poly vs

Reversing a vertex list does not move its carrier.

Polygonal connectedness inside a set

def Schoenflies.PolyConnIn (S : Set Plane) (x y : Plane) : Prop

x and y are joined by a polygonal path lying inside S.

This is the relation exists_poly_of_isPreconnected produces; naming it lets the local statement below be phrased without repeating the vertex-list existential.

Equations

• Schoenflies.PolyConnIn S x y = ∃ (vs : List Schoenflies.Plane) (h : vs ≠ []), Schoenflies.poly vs ⊆ S ∧ vs.head h = x ∧ vs.getLast h = y

The two relations agree

PolyReaches.exists_poly and polyReaches_of_poly_subset are both on main; this is the one-line packaging that lets a producer of either relation serve a consumer of the other.

theorem Schoenflies.polyConnIn_iff_polyReaches {S : Set Plane} {x y : Plane} : PolyConnIn S x y ↔ PolyReaches S x y

The vertex-list relation of LocallyPolygonal.lean and the inductive relation of PolygonalCarrier.lean are the same relation.

theorem Schoenflies.PolyConnIn.polyReaches {S : Set Plane} {x y : Plane} : PolyConnIn S x y → PolyReaches S x y

Alias of the forward direction of Schoenflies.polyConnIn_iff_polyReaches.

---

The vertex-list relation of LocallyPolygonal.lean and the inductive relation of PolygonalCarrier.lean are the same relation.

theorem Schoenflies.PolyReaches.polyConnIn {S : Set Plane} {x y : Plane} : PolyReaches S x y → PolyConnIn S x y

Alias of the reverse direction of Schoenflies.polyConnIn_iff_polyReaches.

---

The vertex-list relation of LocallyPolygonal.lean and the inductive relation of PolygonalCarrier.lean are the same relation.

theorem Schoenflies.PolyConnIn.refl {S : Set Plane} {x : Plane} (hx : x ∈ S) : PolyConnIn S x x

theorem Schoenflies.PolyConnIn.left_mem {S : Set Plane} {x y : Plane} (h : PolyConnIn S x y) : x ∈ S

A point joined to anything lies in the carrier.

theorem Schoenflies.PolyConnIn.right_mem {S : Set Plane} {x y : Plane} (h : PolyConnIn S x y) : y ∈ S

theorem Schoenflies.PolyConnIn.mono {S T : Set Plane} {x y : Plane} (h : PolyConnIn S x y) (hST : S ⊆ T) : PolyConnIn T x y

theorem Schoenflies.PolyConnIn.trans {S : Set Plane} {x y z : Plane} (hxy : PolyConnIn S x y) (hyz : PolyConnIn S y z) : PolyConnIn S x z

theorem Schoenflies.PolyConnIn.symm {S : Set Plane} {x y : Plane} (h : PolyConnIn S x y) : PolyConnIn S y x

theorem Schoenflies.polyConnIn_of_convex {S : Set Plane} {x y : Plane} {C : Set Plane} (hC : Convex ℝ C) (hCS : C ⊆ S) (hx : x ∈ C) (hy : y ∈ C) : PolyConnIn S x y

Convexity is the base case: the segment is already a polygonal path.

theorem Schoenflies.polyConnIn_union_of_convex {x y : Plane} {C D : Set Plane} (hC : Convex ℝ C) (hD : Convex ℝ D) (hmeet : (C ∩ D).Nonempty) (hx : x ∈ C ∪ D) (hy : y ∈ C ∪ D) : PolyConnIn (C ∪ D) x y

Two intersecting convex pieces are joined by segments through a common point.

The local statement

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

S is polygonally connected near p: some open U containing p has all the points of U ∩ S joined to each other by polygonal paths inside S.

U ∩ S is the relative neighbourhood; stating it through an ambient open set avoids carrying a subtype topology. Note the paths are required to lie in S, not in the neighbourhood — that is the form brick B6's clopen argument consumes.

Equations

• Schoenflies.IsLocallyPolyConnAt S p = ∃ (U : Set Schoenflies.Plane), IsOpen U ∧ p ∈ U ∧ ∀ x ∈ U ∩ S, ∀ y ∈ U ∩ S, Schoenflies.PolyConnIn S x y

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

S is locally polygonally connected: polygonally connected near each of its points.

Equations

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

theorem Schoenflies.isLocallyPolyConnAt_of_convex {S U : Set Plane} {p : Plane} (hU : IsOpen U) (hpU : p ∈ U) (hUS : U ⊆ S) (hconv : Convex ℝ U) : IsLocallyPolyConnAt S p

If the relative neighbourhood is itself convex there is nothing to do.

theorem Schoenflies.isLocallyPolyConnAt_of_star {S U : Set Plane} {p : Plane} {ι : Type u_1} {C : ι → Set Plane} (hU : IsOpen U) (hpU : p ∈ U) (hcover : U ∩ S ⊆ ⋃ (i : ι), C i) (hsub : ∀ (i : ι), C i ⊆ S) (hconv : ∀ (i : ι), Convex ℝ (C i)) (hstar : ∀ (i : ι), ∀ z ∈ C i, p ∈ C i) : IsLocallyPolyConnAt S p

The gluing step, and the whole geometric content of the three shapes: if the relative neighbourhood is covered by convex pieces each of which is either empty or contains p, then any two of its points are joined by two segments through p.

No piece is required to be nonempty and no piece is named, so the same statement covers the disk, the half-disk and the three-quarter disk at once.

The four sides of a square

theorem Schoenflies.Plane.mem_openSquare_iff (c : Plane) (r : ℝ) (x : Plane) : x ∈ c.openSquare r ↔ ∀ (i : Fin 2), |x.ofLp i - c.ofLp i| < r

A coordinate description of the open square: it is the set of points within r of the centre in each coordinate separately.

theorem Schoenflies.Plane.mem_openSquare_self {p : Plane} {s : ℝ} (hs : 0 < s) : p ∈ p.openSquare s

The centre of a square of positive radius is in it.

theorem Schoenflies.Plane.openSquare_mono {p : Plane} {s t : ℝ} (h : s ≤ t) : p.openSquare s ⊆ p.openSquare t

Squares about a point grow with the radius.

def Schoenflies.Plane.sideHalfPlane (c : Plane) (r : ℝ) (i : Fin 2) (b : Bool) : Set Plane

The closed half-plane on the far side of the i-th pair of sides of the square about c of radius r; b = true picks the upper one. The four of them cover the complement of the square, and each is convex, which is all the argument uses them for.

Equations

• c.sideHalfPlane r i b = bif b then {x : Schoenflies.Plane | c.ofLp i + r ≤ x.ofLp i} else {x : Schoenflies.Plane | x.ofLp i ≤ c.ofLp i - r}

noncomputable def Schoenflies.Plane.sideGap (c : Plane) (r : ℝ) (p : Plane) (i : Fin 2) (b : Bool) : ℝ

How much room there is between p and the half-plane sideHalfPlane c r i b: positive exactly when p is outside it, and an upper bound on a square radius that keeps a neighbourhood of p clear of it.

Equations

• c.sideGap r p i b = bif b then c.ofLp i + r - p.ofLp i else p.ofLp i - (c.ofLp i - r)

theorem Schoenflies.Plane.convex_sideHalfPlane (c : Plane) (r : ℝ) (i : Fin 2) (b : Bool) : Convex ℝ (c.sideHalfPlane r i b)

theorem Schoenflies.Plane.sideHalfPlane_subset_compl (c : Plane) (r : ℝ) (i : Fin 2) (b : Bool) : c.sideHalfPlane r i b ⊆ (c.openSquare r)ᶜ

Each of the four half-planes misses the open square.

theorem Schoenflies.Plane.compl_openSquare_subset_iUnion (c : Plane) (r : ℝ) : (c.openSquare r)ᶜ ⊆ ⋃ (ib : Fin 2 × Bool), c.sideHalfPlane r ib.1 ib.2

The complement of an open square is covered by the four closed half-planes bounding it.

theorem Schoenflies.Plane.openSquare_disjoint_sideHalfPlane {c : Plane} {r s : ℝ} {p : Plane} {i : Fin 2} {b : Bool} (hs : s ≤ c.sideGap r p i b) (x : Plane) : x ∈ p.openSquare s → x ∉ c.sideHalfPlane r i b

If the radius is at most the room between p and a half-plane, the square about p of that radius misses the half-plane. No sign condition on the gap: when it is nonpositive the radius is too, and the square is empty.

theorem Schoenflies.Plane.mem_sideHalfPlane_of_sideGap_nonpos {c : Plane} {r : ℝ} {p : Plane} {i : Fin 2} {b : Bool} (h : c.sideGap r p i b ≤ 0) : p ∈ c.sideHalfPlane r i b

If there is no room between p and a half-plane, p is in it.

theorem Schoenflies.Plane.convex_openSquare_inter_sideHalfPlane (p : Plane) (s : ℝ) (c : Plane) (r : ℝ) (i : Fin 2) (b : Bool) : Convex ℝ (p.openSquare s ∩ c.sideHalfPlane r i b)

Each piece the sides of one square cut a small square into is an axis-parallel rectangle — an intersection of four coordinate strips with one more coordinate half-plane — and is therefore convex. This is the only property of the three basic shapes the argument uses.

Choosing one radius for finitely many constraints

theorem Schoenflies.exists_pos_le_of_pos {ι : Type u_1} [Finite ι] (d : ι → ℝ) : ∃ s > 0, ∀ (i : ι), 0 < d i → s ≤ d i

A positive lower bound for whichever members of a finite family happen to be positive. This is exists_pos_le_of_finite with the selection built in; the members that are nonpositive impose nothing.

theorem Schoenflies.Plane.exists_radius_sides (c : Plane) (r : ℝ) (p : Plane) : ∃ s > 0, ∀ (ib : Fin 2 × Bool), ∀ z ∈ p.openSquare s ∩ c.sideHalfPlane r ib.1 ib.2, p ∈ p.openSquare s ∩ c.sideHalfPlane r ib.1 ib.2

A radius small enough that the square about p misses every side half-plane of the square about c that p itself is outside of.

The one-square case

theorem Schoenflies.isLocallyPolyConnAt_compl_openSquare (c : Plane) (r : ℝ) (p : Plane) : IsLocallyPolyConnAt (c.openSquare r)ᶜ p

The one-square case of brick B5. The complement of an open axis-parallel square is polygonally connected near every point of the plane.

The neighbourhood is a small square about p; intersected with the complement it becomes the union of the four rectangles cut off by the sides of the big square, each convex and each either empty or containing p. That is the disk / half-disk / three-quarter-disk trichotomy, with the cases never distinguished.

Finitely many squares

theorem Schoenflies.isLocallyPolyConn_compl_biUnion {A : Set Plane} (hA : A.Finite) (ρ : Plane → ℝ) (hdisj : ∀ c ∈ A, ∀ c' ∈ A, c ≠ c' → Disjoint (c.closedSquare (ρ c)) (c'.closedSquare (ρ c'))) : IsLocallyPolyConn (⋃ c ∈ A, c.openSquare (ρ c))ᶜ

Brick B5. The plane minus finitely many open axis-parallel squares whose closed squares are pairwise disjoint is locally polygonally connected.

Two steps. Away from all the closed squares a small square about p is convex and already inside M. Otherwise p lies in exactly one closed square — exactly one, by disjointness — 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 and the previous theorem's decomposition applies verbatim.