A simple arc does not separate the plane

thm:arc-complement. Two points off a simple arc A are covered by a chain of small axis-parallel squares strung along A; the two points lie in the outer face of every consecutive pair of links, hence — by lem:outer-chain — in the outer face of the whole chain, which is an open connected set missing A. lem:polygonal-connected then joins them there.

The single-ambient-graph obligation, and how it is met

Graph.IsPlaneChain requires every link Γ i to be a subgraph of one ambient plane graph with one drawing. A link built as the polygonal overlay of its own squares would not qualify: the total overlay cuts those same segments at the crossings with the squares of other links as well, so a sub-overlay has edges the total overlay has subdivided further.

The construction is therefore inverted. familyPieces c N r is one list holding the four sides of every small square; familyOverlay c N r is the one overlay of that list; and a link is carved out of it by restricting the edge set:

• segGraph S — the plane graph spanned by a set S of straight edges, with the ends of those edges as vertices. overlayGraph pieces points = segGraph {Q | Q ∈ overlayPieces pieces points} holds by rfl, so segGraph_mono turns a subset of the overlay's edges into a subgraph of the overlay with nothing to prove.
• squareGraph pieces points c r — the edges of the overlay lying on the boundary of the square of radius r about c, spanned. It occupies exactly that boundary (pointSet_squareGraph), and every cut point on the boundary is one of its vertices (mem_vertexSet_squareGraph), which is what Graph.IsTwoConnected.union needs.
• familyChain c N m r i — the i-th link: Graph.chainUnion of the m + 1 square graphs of the i-th coarse subarc. Consecutive links share the square at the sample they have in common; nonconsecutive links are disjoint.

isPlaneChain_familyChain is the theorem that this family is a Graph.IsPlaneChain, stated for an arbitrary family of centres c : ℕ → Plane with two geometric hypotheses — consecutive centres closer than one radius, nonconsecutive-block centres further apart than two radii. The arc enters only in exists_face_of_notMem_arc, where c j = α(j/N).

What is assumed

Three hypotheses, all named in the statements that carry them.

• SquaresTwoConnected — the part of a polygonal overlay lying on the boundary of one of its squares is 2-connected. That part is the subdivided boundary cycle of an axis-parallel square: four sides, cut at finitely many interior points, every cut point a vertex, the four corners among the vertices. It is a cycle, so Graph.IsLongCycle.isTwoConnected finishes; what a discharger must build is the cyclic order of the cut points along the four sides, for which Schoenflies/SegmentOrder.lean is the tool. Nothing about the arc, the chain or the outer face enters the statement.
• Graph.CrosscutExists and Graph.CrosscutEncloses — the two halves of the descent step of lem:outer-chain, quoted from Schoenflies/OuterChain.lean unchanged. Because the chain is built from choices made inside the proof of exists_face_of_notMem_arc, they appear there in ∀-form: CrosscutExists conditioned on Graph.IsPlaneChain (which is how a discharger will state it) and CrosscutEncloses for every point.

Blueprint

• segGraph, squareGraph, familyPieces, familyOverlay, familySquare, familyChain — the construction of the proof of thm:arc-complement: "around every sample draw the boundary of the axis-parallel square of ℓ^∞-radius δ/4, and let Γ_i be the polygonal overlay (lem:polygonal-overlay) of the square boundaries associated with A_i".
• familyChain_isTwoConnected — "it follows inductively from lem:union-two-connected that Γ_i is 2-connected".
• isPlaneChain_familyChain — "consecutive graphs Γ_i, Γ_{i+1} share the square at their common sample. If |i-j| ≥ 2, then Γ_i and Γ_j are disjoint".
• outer_of_notMem_closedSquare, outerOnPairs_familyChain — "the graph Γ_i ∪ Γ_{i+1} is contained in the ℓ^∞-square of radius 3d centered at a_i … both p and q lie outside this containing square and hence in the outer face of the pair".
• notMem_face_of_mem_openSquare — "if it lies inside, the boundary cycle of that square separates it from the outer face of G".
• exists_face_of_notMem_arc — the whole proof of thm:arc-complement up to the last sentence.
• isConnected_compl_arc, exists_simple_poly_compl_arc — thm:arc-complement: the complement of a simple arc is connected, and any two of its points are joined in it by a simple polygonal arc.

Part 1: the subgraph of the plane spanned by a set of straight edges

def Schoenflies.segGraph (S : Set Piece) : Graph Plane Piece

The plane graph spanned by a set of straight edges. Its vertices are the ends of those edges and an edge links its two ends in either order — the shape of Schoenflies.overlayGraph, with the edge list replaced by an arbitrary set.

This exists so that a part of one overlay can be spoken about as a graph in its own right while remaining a subgraph of the whole overlay (segGraph_mono). Building the part as an overlay of its own source segments would not do: the total overlay cuts those segments at more points, so a sub-overlay is not a subgraph of it.

Equations

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

@[simp]

theorem Schoenflies.segGraph_vertexSet (S : Set Piece) : (segGraph S).vertexSet = {v : Plane | ∃ P ∈ S, v = P.1 ∨ v = P.2}

@[simp]

theorem Schoenflies.segGraph_edgeSet (S : Set Piece) : (segGraph S).edgeSet = S

@[simp]

theorem Schoenflies.segGraph_isLink {S : Set Piece} {P : Piece} {x y : Plane} : (segGraph S).IsLink P x y ↔ P ∈ S ∧ (x = P.1 ∧ y = P.2 ∨ x = P.2 ∧ y = P.1)

theorem Schoenflies.mem_vertexSet_segGraph {S : Set Piece} {v : Plane} : v ∈ (segGraph S).vertexSet ↔ ∃ P ∈ S, v = P.1 ∨ v = P.2

theorem Schoenflies.mem_vertexSet_segGraph_of_end {S : Set Piece} {P : Piece} {v : Plane} (hP : P ∈ S) (h : v = P.1 ∨ v = P.2) : v ∈ (segGraph S).vertexSet

An end of an edge is a vertex.

theorem Schoenflies.segGraph_mono {S T : Set Piece} (h : S ⊆ T) : segGraph S ≤ segGraph T

More edges, larger graph. This is the whole point of segGraph: the pieces of the chain are subgraphs of one ambient overlay by construction.

theorem Schoenflies.segGraph_finite {S : Set Piece} (hS : S.Finite) : (segGraph S).Finite

theorem Schoenflies.overlayGraph_eq_segGraph (pieces : List Piece) (points : List Plane) : overlayGraph pieces points = segGraph {Q : Piece | Q ∈ overlayPieces pieces points}

The overlay graph is the graph spanned by its own edge list. Definitional, so that a subset of the overlay pieces spans a subgraph of the overlay with nothing to prove.

theorem Schoenflies.pointSet_segGraph (S : Set Piece) : (segGraph S).pointSet segmentDrawing = ⋃ P ∈ S, P.seg

What a spanned graph occupies is the union of its segments: every vertex is an end of an edge, so the vertices add nothing.

Part 2: the part of an overlay lying on one square

The chain graphs are assembled out of these. Each is the set of overlay edges whose segment lies on one small square boundary, spanned by segGraph — so it is a subgraph of the total overlay, not an overlay of the four sides of that square alone.

theorem Schoenflies.exists_overlayPiece_mem_subset {pieces : List Piece} {points : List Plane} {x : Plane} {P₀ : Piece} (hP₀ : P₀ ∈ pieces) (hx : x ∈ P₀.seg) : ∃ Q ∈ overlayPieces pieces points, x ∈ Q.seg ∧ Q.seg ⊆ P₀.seg

Every point of a source segment lies on an overlay edge inside that source segment. Schoenflies.exists_overlayPiece_end_subset is the same statement for a cut point, with the edge pinned so as to have that point among its ends; this is the plain covering form, and it is what makes the part of the overlay on a square occupy the whole of that square's boundary.

def Schoenflies.squareEdges (pieces : List Piece) (points : List Plane) (c : Plane) (r : ℝ) : Set Piece

The edges of an overlay whose segment lies on the boundary of the square of ℓ^∞-radius r about c.

Equations

• Schoenflies.squareEdges pieces points c r = {Q : Schoenflies.Piece | Q ∈ Schoenflies.overlayPieces pieces points ∧ Q.seg ⊆ frontier (c.closedSquare r)}

def Schoenflies.squareGraph (pieces : List Piece) (points : List Plane) (c : Plane) (r : ℝ) : Graph Plane Piece

The part of one overlay lying on one square boundary. A subgraph of that overlay by construction (squareGraph_le), which is the single-ambient-graph obligation of Graph.IsPlaneChain discharged at the bottom of the tower.

Equations

• Schoenflies.squareGraph pieces points c r = Schoenflies.segGraph (Schoenflies.squareEdges pieces points c r)

theorem Schoenflies.squareEdges_finite {pieces : List Piece} {points : List Plane} {c : Plane} {r : ℝ} : (squareEdges pieces points c r).Finite

theorem Schoenflies.squareGraph_le {pieces : List Piece} {points : List Plane} {c : Plane} {r : ℝ} : squareGraph pieces points c r ≤ overlayGraph pieces points

instance Schoenflies.squareGraph_finite {pieces : List Piece} {points : List Plane} {c : Plane} {r : ℝ} : (squareGraph pieces points c r).Finite

theorem Schoenflies.pointSet_squareGraph_subset {pieces : List Piece} {points : List Plane} {c : Plane} {r : ℝ} : (squareGraph pieces points c r).pointSet segmentDrawing ⊆ frontier (c.closedSquare r)

theorem Schoenflies.pointSet_squareGraph {pieces : List Piece} {points : List Plane} {c : Plane} {r : ℝ} (hr : 0 ≤ r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) : (squareGraph pieces points c r).pointSet segmentDrawing = frontier (c.closedSquare r)

The part of the overlay on a square occupies the whole square boundary. Every point of the boundary lies on one of the four sides, and the overlay subdivides that side into pieces that stay inside it.

theorem Schoenflies.mem_vertexSet_squareGraph {pieces : List Piece} {points : List Plane} {c : Plane} {r : ℝ} (hnd : ∀ P ∈ pieces, P.Nondeg) (hr : 0 ≤ r) (hsub : ∀ P ∈ squarePieces c r, P ∈ pieces) {z : Plane} (hz : z ∈ points) (hzf : z ∈ frontier (c.closedSquare r)) : z ∈ (squareGraph pieces points c r).vertexSet

A cut point on a square boundary is a vertex of the part of the overlay on that square. This is what turns "two nearby squares meet in two points" into the two common vertices that Graph.IsTwoConnected.union consumes.

theorem Schoenflies.exists_two_vertices_squareGraph {pieces : List Piece} {points : List Plane} {c₁ c₂ : Plane} {r : ℝ} (hnd : ∀ P ∈ pieces, P.Nondeg) (hMeets : MeetsAreCut pieces points) (hr : 0 < r) (hd : c₁.supDist c₂ < r) (h₁ : ∀ P ∈ squarePieces c₁ r, P ∈ pieces) (h₂ : ∀ P ∈ squarePieces c₂ r, P ∈ pieces) : ∃ (a : Plane) (b : Plane), a ≠ b ∧ a ∈ (squareGraph pieces points c₁ r).vertexSet ∧ a ∈ (squareGraph pieces points c₂ r).vertexSet ∧ b ∈ (squareGraph pieces points c₁ r).vertexSet ∧ b ∈ (squareGraph pieces points c₂ r).vertexSet

Two nearby congruent squares contribute two common vertices, each a vertex of the part of the overlay lying on its own square. With equal centres this produces two vertices of one square, which is how consecutive links of the chain are shown to meet.

Part 3: the chain of square boundaries

Everything here is about a family of centres c : ℕ → Plane and one radius r; the arc enters only in Part 5, where c j = α (j / N). Separating the two keeps the single-ambient-graph bookkeeping free of parametrisation arithmetic.

noncomputable def Schoenflies.familyPieces (c : ℕ → Plane) (N : ℕ) (r : ℝ) : List Piece

The one list of source segments: the four sides of the square of ℓ^∞-radius r about each of the centres c 0, …, c N.

The whole proof rests on this being one list. A chain link built as the overlay of its own squares would not be a subgraph of the total overlay, because the total overlay cuts those segments at the crossings with squares of other links as well.

Equations

• Schoenflies.familyPieces c N r = List.flatMap (fun (j : ℕ) => Schoenflies.squarePieces (c j) r) (List.range (N + 1))

theorem Schoenflies.mem_familyPieces {r : ℝ} {c : ℕ → Plane} {N : ℕ} {P : Piece} : P ∈ familyPieces c N r ↔ ∃ j ≤ N, P ∈ squarePieces (c j) r

theorem Schoenflies.squarePieces_subset_familyPieces {r : ℝ} {c : ℕ → Plane} {N j : ℕ} (hj : j ≤ N) (P : Piece) : P ∈ squarePieces (c j) r → P ∈ familyPieces c N r

theorem Schoenflies.familyPieces_nondeg {r : ℝ} {c : ℕ → Plane} {N : ℕ} (hr : 0 < r) (P : Piece) : P ∈ familyPieces c N r → P.Nondeg

noncomputable def Schoenflies.familyPoints (c : ℕ → Plane) (N : ℕ) (r : ℝ) : List Plane

The cut points of that list, chosen once and for all. Schoenflies.exists_cut_points produces them existentially; naming them here is what lets every chain link be a subgraph of the same overlay.

Equations

• Schoenflies.familyPoints c N r = ⋯.choose

theorem Schoenflies.familyPoints_endsAreCut {r : ℝ} {c : ℕ → Plane} {N : ℕ} : EndsAreCut (familyPieces c N r) (familyPoints c N r)

theorem Schoenflies.familyPoints_meetsAreCut {r : ℝ} {c : ℕ → Plane} {N : ℕ} : MeetsAreCut (familyPieces c N r) (familyPoints c N r)

noncomputable def Schoenflies.familyOverlay (c : ℕ → Plane) (N : ℕ) (r : ℝ) : Graph Plane Piece

The single ambient plane graph of the whole proof: the polygonal overlay of every small square at once (lem:polygonal-overlay).

Equations

• Schoenflies.familyOverlay c N r = Schoenflies.overlayGraph (Schoenflies.familyPieces c N r) (Schoenflies.familyPoints c N r)

noncomputable def Schoenflies.familySquare (c : ℕ → Plane) (N : ℕ) (r : ℝ) (j : ℕ) : Graph Plane Piece

The part of the ambient overlay lying on the j-th small square.

Equations

• Schoenflies.familySquare c N r j = Schoenflies.squareGraph (Schoenflies.familyPieces c N r) (Schoenflies.familyPoints c N r) (c j) r

noncomputable def Schoenflies.familyChain (c : ℕ → Plane) (N m : ℕ) (r : ℝ) (i : ℕ) : Graph Plane Piece

The i-th link of the chain, Γ_i: the squares at the m + 1 fine samples i·m, …, i·m + m of the i-th coarse subarc. Consecutive links share the square at the sample they have in common.

Equations

• Schoenflies.familyChain c N m r i = Graph.chainUnion (Schoenflies.familySquare c N r) (i * m) m

theorem Schoenflies.familySquare_le {r : ℝ} {c : ℕ → Plane} {N j : ℕ} : familySquare c N r j ≤ familyOverlay c N r

instance Schoenflies.familySquare_finite {r : ℝ} {c : ℕ → Plane} {N j : ℕ} : (familySquare c N r j).Finite

theorem Schoenflies.familyChain_le {r : ℝ} {c : ℕ → Plane} {N m i : ℕ} : familyChain c N m r i ≤ familyOverlay c N r

theorem Schoenflies.familyChain_finite {r : ℝ} {c : ℕ → Plane} {N m i : ℕ} : (familyChain c N m r i).Finite

theorem Schoenflies.familyOverlay_isDrawing {r : ℝ} {c : ℕ → Plane} {N : ℕ} (hr : 0 < r) : (familyOverlay c N r).IsDrawing segmentDrawing

The drawing of the ambient overlay: every edge is a straight segment.

theorem Schoenflies.pointSet_familySquare {r : ℝ} {c : ℕ → Plane} {N j : ℕ} (hr : 0 < r) (hj : j ≤ N) : (familySquare c N r j).pointSet segmentDrawing = frontier ((c j).closedSquare r)

theorem Schoenflies.exists_mem_frontier_of_mem_pointSet_familyChain {r : ℝ} {c : ℕ → Plane} {N m i : ℕ} {z : Plane} (hz : z ∈ (familyChain c N m r i).pointSet segmentDrawing) : ∃ (j : ℕ), i * m ≤ j ∧ j ≤ i * m + m ∧ z ∈ frontier ((c j).closedSquare r)

A point of a chain link lies on one of that link's squares.

def Schoenflies.SquaresTwoConnected : Prop

Assumed: the part of a polygonal overlay lying on the boundary of one of its squares is 2-connected.

It is the subdivided boundary of an axis-parallel square — four sides, cut at finitely many points, each cut point a vertex — so it is a cycle, and Graph.IsLongCycle.isTwoConnected finishes. What a discharging module must build is the cyclic order of the cut points along the four sides; Schoenflies/SegmentOrder.lean is the tool. Nothing about the arc, the chain or the outer face enters the statement.

Equations

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

theorem Schoenflies.familySquare_isTwoConnected {r : ℝ} {c : ℕ → Plane} {N j : ℕ} (h2c : SquaresTwoConnected) (hr : 0 < r) (hj : j ≤ N) : (familySquare c N r j).IsTwoConnected

theorem Schoenflies.exists_two_vertices_familySquare {r : ℝ} {c : ℕ → Plane} {N : ℕ} (hr : 0 < r) {j j' : ℕ} (hj : j ≤ N) (hj' : j' ≤ N) (hd : (c j).supDist (c j') < r) : ∃ (a : Plane) (b : Plane), a ≠ b ∧ a ∈ (familySquare c N r j).vertexSet ∧ a ∈ (familySquare c N r j').vertexSet ∧ b ∈ (familySquare c N r j).vertexSet ∧ b ∈ (familySquare c N r j').vertexSet

Two squares whose centres are within one radius contribute two common vertices to the two parts of the overlay lying on them. With equal centres this gives two vertices of one square, which is how consecutive links of the chain are shown to meet.

theorem Schoenflies.familyChain_isTwoConnected {r : ℝ} {c : ℕ → Plane} {N m i : ℕ} (h2c : SquaresTwoConnected) (hr : 0 < r) (hi : i * m + m ≤ N) (hstep : ∀ q < N, (c q).supDist (c (q + 1)) < r) : (familyChain c N m r i).IsTwoConnected

Each link of the chain is 2-connected: consecutive squares in it share two vertices, so lem:union-two-connected applies all the way along.

Part 4: the chain satisfies Graph.IsPlaneChain

This is the obligation Schoenflies/OuterChain.lean flagged: every link must be a subgraph of one ambient plane graph with one drawing. It is discharged by construction — every link is a Graph.chainUnion of familySquares, and every familySquare is a segGraph on a subset of the edges of the one overlay familyOverlay c N r.

theorem Schoenflies.isPlaneChain_familyChain {r : ℝ} {c : ℕ → Plane} {N m n : ℕ} (h2c : SquaresTwoConnected) (hr : 0 < r) (hn : 2 ≤ n) (hN : n * m + m ≤ N) (hstep : ∀ q < N, (c q).supDist (c (q + 1)) < r) (hfar : ∀ (p q : ℕ), p ≤ n → q ≤ n → p + 1 < q → ∀ (j : ℕ), p * m ≤ j → j ≤ p * m + m → ∀ (j' : ℕ), q * m ≤ j' → j' ≤ q * m + m → 2 * r < (c j).supDist (c j')) : Graph.IsPlaneChain (familyChain c N m r) segmentDrawing (familyOverlay c N r) n

The chain of square boundaries is a plane chain.

The two geometric hypotheses are the blueprint's: consecutive centres are closer than one square radius (hstep), and centres belonging to nonconsecutive links are more than two radii apart (hfar). Everything else — one ambient graph, one drawing, finiteness, polygonality — is discharged by the construction.

Part 5: the outer face of the chain

Two plane facts, both general, and then the hypothesis of lem:outer-chain on consecutive pairs.

theorem Schoenflies.outer_of_notMem_closedSquare {β : Type u_1} {G : Graph Plane β} {drawing : β → ℝ → Plane} {c₀ : Plane} {R : ℝ} (hsub : G.pointSet drawing ⊆ c₀.closedSquare R) {base : Plane} (hbase : base ∉ c₀.closedSquare R) : base ∈ G.exterior drawing ∧ ¬Bornology.IsBounded (G.face drawing base)

The outside of a square containing the whole drawing lies in one unbounded face. Graph.beyondSquare_subset_face is this statement for a square centred at the origin; the chain argument needs it about a square centred at a sample of the arc, and the connectedness of the outside of an arbitrary square is Plane.isConnected_compl_closedSquare.

theorem Schoenflies.connectedComponentIn_compl_frontier_closedSquare {c₀ : Plane} {R : ℝ} {z : Plane} (hz : z ∈ c₀.openSquare R) : connectedComponentIn (frontier (c₀.closedSquare R))ᶜ z = c₀.openSquare R

The complement of a square's boundary has the open square as one whole component.

theorem Schoenflies.notMem_face_of_mem_openSquare {β : Type u_1} {G : Graph Plane β} {drawing : β → ℝ → Plane} {c₀ : Plane} {R : ℝ} (hfr : frontier (c₀.closedSquare R) ⊆ G.pointSet drawing) {base z : Plane} (hb : ¬Bornology.IsBounded (G.face drawing base)) (hz : z ∈ c₀.openSquare R) : z ∉ G.face drawing base

"If it lies inside, the boundary cycle of that square separates it from the outer face." A point strictly inside a square whose boundary the drawing carries is not in any unbounded face: the face would be a connected subset of the complement of that boundary meeting the inside, hence inside, hence bounded.

theorem Schoenflies.outerOnPairs_familyChain {r : ℝ} {c : ℕ → Plane} {N m n : ℕ} {R : ℝ} {x : Plane} (hcontain : ∀ (p : ℕ), p + 1 ≤ n → ∀ (j : ℕ), p * m ≤ j → j ≤ p * m + m + m → (c j).supDist (c (p * m)) + r ≤ R) (hx : ∀ (p : ℕ), p + 1 ≤ n → R < x.supDist (c (p * m))) : Graph.OuterOnPairs (familyChain c N m r) segmentDrawing n x

The hypothesis of lem:outer-chain on consecutive pairs. Every consecutive pair of links is contained in one square of radius R about the pair's first centre, and x is outside that square.

theorem Schoenflies.outer_face_familyChain {r : ℝ} {c : ℕ → Plane} {N m n : ℕ} {x : Plane} (hchain : Graph.IsPlaneChain (familyChain c N m r) segmentDrawing (familyOverlay c N r) n) (hout : Graph.OuterOnPairs (familyChain c N m r) segmentDrawing n x) : x ∈ (Graph.chainUnion (familyChain c N m r) 0 n).exterior segmentDrawing ∧ ¬Bornology.IsBounded ((Graph.chainUnion (familyChain c N m r) 0 n).face segmentDrawing x)

lem:outer-chain, applied to the chain of squares. Stated with the two halves of the descent step exactly as Schoenflies/OuterChain.lean defines them and for this chain, so that a discharger's terms substitute here with nothing to adapt.

Part 6: from the Euclidean distance to the sup distance

The only place the two metrics have to be compared. ‖·‖ ≤ √2‖·‖∞ and √2 < 2, so half the Euclidean distance is a strict lower bound for the sup distance — which is what turns the blueprint's separation constants into square radii.

theorem Schoenflies.lt_supDist_of_le_dist {x y : Plane} {t : ℝ} (ht : 0 < t) (h : t ≤ dist x y) : t / 2 < x.supDist y

theorem Schoenflies.sample_mem_Icc_of_block {K m j p : ℕ} (hm : 0 < m) (h₁ : p * m ≤ j) (h₂ : j ≤ (p + 1) * m) : sample (K * m) j ∈ Set.Icc (sample K p) (sample K (p + 1))

The block of fine samples belonging to one coarse cell lies in that coarse cell.

theorem Schoenflies.exists_block_index {j m n : ℕ} (hj : j ≤ (n + 1) * m) : ∃ i ≤ n, i * m ≤ j ∧ j ≤ i * m + m

Every index below (n+1)·m belongs to one of the n + 1 blocks of length m.

Part 7: thm:arc-complement

The blueprint's proof, in its own order. The two hypotheses hce and hcen are the two halves of the descent step of lem:outer-chain, quoted verbatim from Schoenflies/OuterChain.lean; h2c is the 2-connectivity of one subdivided square, discussed at SquaresTwoConnected.

theorem Schoenflies.exists_face_of_notMem_arc {A : Set Plane} (hA : IsArc A) (h2c : SquaresTwoConnected) {u w : Plane} (hu : u ∉ A) (hw : w ∉ A) : ∃ (F : Set Plane), IsOpen F ∧ IsConnected F ∧ u ∈ F ∧ w ∈ F ∧ Disjoint F A

The heart of thm:arc-complement: two points off a simple arc lie in a common open connected set missing the arc — the outer face of the chain of small squares along the arc.

theorem Schoenflies.exists_simple_poly_compl_arc {A : Set Plane} (hA : IsArc A) (h2c : SquaresTwoConnected) {u w : Plane} (huw : u ≠ w) (hu : u ∉ A) (hw : w ∉ A) : ∃ (P : Set Plane), IsPolygonal P ∧ IsArcBetween P u w ∧ P ⊆ Aᶜ

thm:arc-complement, the polygonal half. Two distinct points off a simple arc are joined, off the arc, by a simple polygonal arc. This is the form lem:accessible-dense consumes; the joining is lem:polygonal-connected inside the outer face.

theorem Schoenflies.isConnected_compl_arc {A : Set Plane} (hA : IsArc A) (h2c : SquaresTwoConnected) : IsConnected Aᶜ

thm:arc-complement. The complement of a simple arc in the plane is connected.