Continuity at the Jordan curve, and thm:square-extension

The last three statements of the manuscript: lem:crosscut-side-correspondence, prop:boundary-continuity, and the assembly of thm:square-extension from them.

Schoenflies/BoundaryContinuity.lean proves the statement with the real combinatorial content, lem:skeleton-crosscuts (Graph.IsStageOn.exists_crosscut), for one finite plane graph. This module takes the crosscuts as given and finishes the section.

The construction inputs

This module isolates the construction-dependent data as explicit hypotheses. They are supplied for the quantitative stage recursion in Schoenflies/InteriorHomeomorphism.lean and Schoenflies/BoundaryAnchors.lean. Nothing else is assumed: thm:jordan and thm:general-crosscut are used through Schoenflies/JordanClosed.lean, where their hypotheses are supplied.

• prop:interior-homeomorphism enters as IsHomeoOn F F' (inside C) (Plane.openSquare 0 1) — the Schoenflies.IsHomeoOn shape of Schoenflies/Inversion.lean: a map, a named inverse, and the continuity and inverse laws on the two sets.
• lem:skeleton-crosscuts + prop:skeleton-agreement enter as Schoenflies.HasAnchorCrosscuts: for two distinct anchors a, b a crosscut P of C from a to b, a crosscut P' of Q° from u a to u b, and the agreement F '' (P ∖ {a,b}) = P' ∖ {u a, u b}. This is exactly what the finite skeleton homeomorphism produces once Graph.IsStageOn.exists_crosscut has been run in the stage containing a and b (see Graph.IsStageOn.exists_isCrosscut below, which does the packaging).
• lem:anchor-density enters as the two clauses 𝒜 ⊆ C and C ⊆ closure 𝒜, plus its "incident with a nonboundary edge" clause in the germ form Schoenflies.HasSpokes: at an anchor c, arbitrarily small connected pieces J of the Jordan domain which cling to c and whose F-images cling to u c. That is the initial subarc of the spoke at c, and its image, which is the initial subarc of the target spoke — the only use the blueprint makes of the spokes, in the paragraph of lem:crosscut-side-correspondence beginning "Choose c ∈ 𝒜 in the relative interior of Aᵢ".

Schoenflies.HasLimitHomeomorphism bundles the four over all curves, and Schoenflies.squareExtension_of_hasLimitHomeomorphism derives Schoenflies.SquareExtension — the exact def of Schoenflies/Endgame.lean — from it. The proof of HasLimitHomeomorphism assembled in Schoenflies/JordanSchoenflies.lean closes the full theorem.

The two arguments

Which side maps to which side is Schoenflies.crosscut_side_correspondence. The homeomorphism of the interiors carries Int(C) ∖ P onto Q° ∖ P' (Schoenflies.image_inside_sdiff), hence carries each of the two components onto one of the two; the labels are pinned by a spoke germ J at an anchor c in the relative interior of A₁. J is connected, misses P because it is small and c ∉ P, so it lies in one side; c ∈ closure J and closure(Uᵢ) ∩ C = Aᵢ force that side to be U₁. The same two facts on the target, applied to F '' J, force F '' U₁ to be U'₁.

Boundary continuity is Schoenflies.tendsto_nhdsWithin_inside. The blueprint argues on a subsequence; the filter form of the same argument avoids extracting one. If F does not tend to u p along 𝓝[Int C] p, then l' = 𝓝[Int C] p ⊓ 𝓟 (F⁻¹ Wᶜ) is a nonzero filter for some open W ∋ u p, and compactness of Q gives a cluster point q ∈ Wᶜ of F along l'. If q ∈ Q° then pushing l' through F' shows p = F' q ∈ Int(C), impossible. Otherwise q ∈ S; anchors a, b separating p from r = u⁻¹ q give a crosscut whose p-side contains every point of Int(C) near p, so l' sits on that side, so q lies in the closure of the corresponding target side, whose trace on S is u(A₁) — and r ∉ A₁.

Blueprint

• Graph.IsStageOn.exists_isCrosscut — lem:skeleton-crosscuts repackaged as Schoenflies.IsCrosscut, the form thm:general-crosscut consumes.
• Schoenflies.IsCutPair.separates, Schoenflies.exists_separating_anchors — the selection step of prop:boundary-continuity: two anchors putting two prescribed points of the curve on opposite arcs. Uses lem:anchor-density through the density hypothesis alone.
• Schoenflies.IsCrosscut.image_of_injOn, Schoenflies.image_sdiff_eq_of_eqOn — the two steps a consumer performs to discharge Schoenflies.HasAnchorCrosscuts from a finite skeleton homeomorphism. No blueprint statement of their own; they are the second paragraph of the proof of lem:skeleton-crosscuts, "the finite skeleton homeomorphism sends P to a simple path P'".
• Schoenflies.crosscut_side_correspondence — lem:crosscut-side-correspondence.
• Schoenflies.extendByBoundary, Schoenflies.tendsto_nhdsWithin_inside, Schoenflies.boundary_continuity — prop:boundary-continuity.
• Schoenflies.isHomeoOn_extendByBoundary, Schoenflies.squareExtension_of_hasLimitHomeomorphism — thm:square-extension.

theorem Graph.IsStageOn.exists_isCrosscut {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {C : Set Schoenflies.Plane} [G.Finite] (h : G.IsStageOn drawing C (Schoenflies.inside C)) (hC : Schoenflies.IsJordanCurve C) {a b : Schoenflies.Plane} (hab : a ≠ b) (haC : a ∈ C) (hbC : b ∈ C) (ha : ∃ (e : β), G.Inc e a ∧ Nonboundary drawing C e) (hb : ∃ (e : β), G.Inc e b ∧ Nonboundary drawing C e) : ∃ P ⊆ G.pointSet drawing, Schoenflies.IsCrosscut C P a b

lem:skeleton-crosscuts, packaged for thm:general-crosscut. The crosscut that Graph.IsStageOn.exists_crosscut extracts from a stage drawn in the closed Jordan domain is a Schoenflies.IsCrosscut of C, which is the configuration every consumer downstream takes.

This is only a repackaging; all the work is in Schoenflies/BoundaryContinuity.lean.

Two elementary facts about the model square

Q° = Int(S): the open square is the Jordan domain of the model curve. This is the bridge between the shape prop:interior-homeomorphism is stated in (a homeomorphism onto Plane.openSquare 0 1) and the shape thm:general-crosscut speaks in (inside modelCurve).

theorem Schoenflies.inside_modelCurve : inside modelCurve = Plane.openSquare 0 1

The Jordan domain of the model curve is the open square.

theorem Schoenflies.isCompact_closedSquare (c : Plane) (r : ℝ) : IsCompact (c.closedSquare r)

The closed square is compact.

Pushing arcs forward

lem:crosscut-side-correspondence labels the target sides by u(A₁) and u(A₂), so the two target arcs have to be produced as images. Nothing here is specific to the square.

theorem Schoenflies.IsArcBetween.image_of_injOn {A S : Set Plane} {p q : Plane} {f : Plane → Plane} (h : IsArcBetween A p q) (hAS : A ⊆ S) (hcont : ContinuousOn f S) (hinj : Set.InjOn f S) : IsArcBetween (f '' A) (f p) (f q)

The image of an arc under a map continuous and injective on a set containing it.

theorem Schoenflies.IsCutPair.image {C A₁ A₂ : Set Plane} {a b : Plane} {f : Plane → Plane} (h : IsCutPair C a b A₁ A₂) (hcont : ContinuousOn f C) (hinj : Set.InjOn f C) : IsCutPair (f '' C) (f a) (f b) (f '' A₁) (f '' A₂)

The image of a cut pair.

theorem Schoenflies.IsCutPair.image_of_isHomeoOn {C A₁ A₂ : Set Plane} {u v : Plane → Plane} {a b : Plane} {T : Set Plane} (h : IsCutPair C a b A₁ A₂) (hu : IsHomeoOn u v C T) : IsCutPair T (u a) (u b) (u '' A₁) (u '' A₂)

The image of a cut pair under a restricted homeomorphism, in the form the target side of lem:crosscut-side-correspondence needs it.

Anchors that separate

The selection step of prop:boundary-continuity. Given two distinct points p, r of the curve and a dense set 𝒜 of anchors, we need anchors a, b with p and r on opposite arcs of C from a to b. Density produces one anchor on each of the two open arcs of C from p to r; the separation is then automatic, because an arc from a to b avoiding p and r would be a connected subset of C ∖ {p, r} meeting both of its two (relatively open) halves.

theorem Schoenflies.exists_anchor_mem_arc {C 𝒜 A₁ A₂ : Set Plane} {a b : Plane} (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hcut : IsCutPair C a b A₁ A₂) : ∃ c ∈ 𝒜, c ∈ A₁ ∧ c ∉ A₂

A dense set meets the relative interior of either arc of a cut pair. The one use lem:anchor-density is put to.

theorem Schoenflies.IsCutPair.separates {C A₁ A₂ B₁ B₂ : Set Plane} {a b p r : Plane} (hB : IsCutPair C p r B₁ B₂) (hA : IsCutPair C a b A₁ A₂) (ha' : a ∉ B₂) (hb' : b ∉ B₁) : p ∈ A₁ ∧ r ∈ A₂ ∨ p ∈ A₂ ∧ r ∈ A₁

Two anchors on opposite open arcs separate. If a lies on the open arc B₁ ∖ {p, r} and b on the opposite one, then any pair of arcs cutting C at a and b puts p and r on different arcs.

The proof is the one separation argument of the section: an arc from a to b missing both p and r is a connected subset of C ∖ {p, r} = (C ∖ B₂) ∪ (C ∖ B₁), a union of two relatively open pieces, and it meets both — because a is in the first and b in the second.

theorem Schoenflies.exists_separating_anchors {C 𝒜 : Set Plane} {p r : Plane} (hC : IsJordanCurve C) (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hp : p ∈ C) (hr : r ∈ C) (hpr : p ≠ r) : ∃ a ∈ 𝒜, ∃ b ∈ 𝒜, ∃ (A₁ : Set Plane) (A₂ : Set Plane), a ≠ b ∧ IsCutPair C a b A₁ A₂ ∧ p ∈ A₁ ∧ p ∉ A₂ ∧ r ∈ A₂ ∧ r ∉ A₁

The selection step of prop:boundary-continuity. Two distinct points of the curve are separated by two anchors of any dense set of anchors.

The hypotheses

Two predicates, one for each thing that is still being built. Both are statements about one curve, so a consumer can discharge them curve by curve.

def Schoenflies.HasAnchorCrosscuts (C 𝒜 : Set Plane) (u F : Plane → Plane) : Prop

lem:skeleton-crosscuts together with prop:skeleton-agreement, as lem:crosscut-side-correspondence consumes them: any two distinct anchors are joined by a crosscut P of C, whose image under the limit map is a crosscut P' of the open square from u a to u b.

The agreement clause is stated on P ∖ {a, b}, which by IsCrosscut.inter_eq is exactly P ∩ Int(C) — the part of the crosscut on which F is defined at all.

Equations

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

def Schoenflies.HasSpokes (C 𝒜 : Set Plane) (u F : Plane → Plane) : Prop

The spokes at the anchors. At an anchor c there are arbitrarily small connected pieces J of the Jordan domain clinging to c whose F-images cling to u c.

This is the germ of the nonboundary edge that lem:anchor-density attaches to c: J is an initial subarc of that edge with the endpoint c removed, and F '' J is the corresponding initial subarc of the target edge, which ends at u c because the finite skeleton homeomorphism sends c to u c. Nothing else about the spokes is used anywhere.

Equations

• Schoenflies.HasSpokes C 𝒜 u F = ∀ c ∈ 𝒜, ∀ ε > 0, ∃ J ⊆ Schoenflies.inside C, IsPreconnected J ∧ J ⊆ Metric.ball c ε ∧ c ∈ closure J ∧ u c ∈ closure (F '' J)

Discharging HasAnchorCrosscuts from a skeleton homeomorphism

The two steps a consumer has to perform, isolated so that they need not be reinvented: the image of a crosscut under the finite skeleton homeomorphism is again a crosscut, and the agreement clause follows from agreement of the limit map with that homeomorphism on the crosscut. Neither says anything about the square, so both apply to the source and the target side of any of the stages.

theorem Schoenflies.IsCrosscut.image_of_injOn {C P : Set Plane} {a b : Plane} {C' Sk : Set Plane} {g : Plane → Plane} (hP : IsCrosscut C P a b) (hPSk : P ⊆ Sk) (hcont : ContinuousOn g Sk) (hinj : Set.InjOn g Sk) (hC' : IsJordanCurve C') (hpoly : IsPolygonal (g '' P)) (ha : g a ∈ C') (hb : g b ∈ C') (hint : g '' (P \ {a, b}) ⊆ inside C') : IsCrosscut C' (g '' P) (g a) (g b)

The image of a crosscut is a crosscut. All that is asked of the map is continuity and injectivity on a set containing the crosscut, plus the two clauses that are genuinely about the target configuration: the image is polygonal, and everything but its two endpoints lies in the target Jordan domain.

theorem Schoenflies.image_sdiff_eq_of_eqOn {P : Set Plane} {F : Plane → Plane} {a b : Plane} {Sk : Set Plane} {g : Plane → Plane} (hPSk : P ⊆ Sk) (hinj : Set.InjOn g Sk) (ha : a ∈ P) (hb : b ∈ P) (hFg : Set.EqOn F g (P \ {a, b})) : F '' (P \ {a, b}) = g '' P \ {g a, g b}

The agreement clause of Schoenflies.HasAnchorCrosscuts, from agreement of the limit map with the skeleton homeomorphism on the part of the crosscut that lies in the domain.

lem:crosscut-side-correspondence

theorem Schoenflies.inside_sdiff_crosscut {C P : Set Plane} {a b : Plane} (h : IsCrosscut C P a b) : inside C \ P = inside C \ (P \ {a, b})

Removing a crosscut from the Jordan domain is the same as removing its interior: the two endpoints are on the curve and so are not in the domain to begin with.

theorem Schoenflies.image_inside_sdiff {C P P' : Set Plane} {u F F' : Plane → Plane} {a b : Plane} (hF : IsHomeoOn F F' (inside C) (Plane.openSquare 0 1)) (hP : IsCrosscut C P a b) (hP' : IsCrosscut modelCurve P' (u a) (u b)) (hagree : F '' (P \ {a, b}) = P' \ {u a, u b}) : F '' (inside C \ P) = inside modelCurve \ P'

The limit map carries Int(C) ∖ P onto Q° ∖ P'. This is the whole use made of prop:skeleton-agreement: it turns a homeomorphism of the interiors into a homeomorphism of the cut interiors.

theorem Schoenflies.image_crosscut_side_subset {C 𝒜 A₁ A₂ P P' : Set Plane} {u v F F' : Plane → Plane} {a b : Plane} (hu : IsHomeoOn u v C modelCurve) (hF : IsHomeoOn F F' (inside C) (Plane.openSquare 0 1)) (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hspoke : HasSpokes C 𝒜 u F) (hcut : IsCutPair C a b A₁ A₂) (hP : IsCrosscut C P a b) (hP' : IsCrosscut modelCurve P' (u a) (u b)) (hagree : F '' (P \ {a, b}) = P' \ {u a, u b}) : F '' inside (A₁ ∪ P) ⊆ inside (u '' A₁ ∪ P')

lem:crosscut-side-correspondence, one inclusion. The side of the crosscut whose closure meets C in A₁ is carried into the side of the target crosscut whose closure meets S in u(A₁).

This is where the spokes are used, and the only place.

theorem Schoenflies.crosscut_side_correspondence {C 𝒜 A₁ A₂ P P' : Set Plane} {u v F F' : Plane → Plane} {a b : Plane} (hu : IsHomeoOn u v C modelCurve) (hF : IsHomeoOn F F' (inside C) (Plane.openSquare 0 1)) (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hspoke : HasSpokes C 𝒜 u F) (hcut : IsCutPair C a b A₁ A₂) (hP : IsCrosscut C P a b) (hP' : IsCrosscut modelCurve P' (u a) (u b)) (hagree : F '' (P \ {a, b}) = P' \ {u a, u b}) : F '' inside (A₁ ∪ P) = inside (u '' A₁ ∪ P') ∧ F '' inside (A₂ ∪ P) = inside (u '' A₂ ∪ P')

lem:crosscut-side-correspondence. The limit map carries each side of a crosscut onto the side of the target crosscut carrying the corresponding boundary arc.

The sides are named the way Schoenflies.crosscut_theorem names them: inside (Aᵢ ∪ P) is the component of Int(C) ∖ P whose closure meets C exactly in Aᵢ.

prop:boundary-continuity

noncomputable def Schoenflies.extendByBoundary (C : Set Plane) (u F : Plane → Plane) : Plane → Plane

The blueprint's Fbar: the limit map on the Jordan domain and the boundary homeomorphism on the curve. It is Schoenflies.paste, which comes with its two evaluation lemmas.

Equations

• Schoenflies.extendByBoundary C u F = Schoenflies.paste C u F

theorem Schoenflies.extendByBoundary_of_mem {C : Set Plane} {u F : Plane → Plane} {z : Plane} (hz : z ∈ C) : extendByBoundary C u F z = u z

theorem Schoenflies.extendByBoundary_of_notMem {C : Set Plane} {u F : Plane → Plane} {z : Plane} (hz : z ∉ C) : extendByBoundary C u F z = F z

theorem Schoenflies.tendsto_nhdsWithin_inside {C 𝒜 : Set Plane} {u v F F' : Plane → Plane} {p : Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) (hF : IsHomeoOn F F' (inside C) (Plane.openSquare 0 1)) (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hcross : HasAnchorCrosscuts C 𝒜 u F) (hspoke : HasSpokes C 𝒜 u F) (hp : p ∈ C) : Filter.Tendsto F (nhdsWithin p (inside C)) (nhds (u p))

prop:boundary-continuity, the substance. Approaching a point p of the curve from inside, the limit map tends to u p.

The blueprint extracts a subsequence; the same argument runs on the filter l' = 𝓝[Int C] p ⊓ 𝓟 (F⁻¹ Wᶜ) without extracting one.

theorem Schoenflies.boundary_continuity {C 𝒜 : Set Plane} {u v F F' : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) (hF : IsHomeoOn F F' (inside C) (Plane.openSquare 0 1)) (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hcross : HasAnchorCrosscuts C 𝒜 u F) (hspoke : HasSpokes C 𝒜 u F) : ContinuousOn (extendByBoundary C u F) (C ∪ inside C)

prop:boundary-continuity. The glued map is continuous on the closed Jordan domain.

thm:square-extension

theorem Schoenflies.isHomeoOn_extendByBoundary {C 𝒜 : Set Plane} {u v F F' : Plane → Plane} (hC : IsJordanCurve C) (hu : IsHomeoOn u v C modelCurve) (hF : IsHomeoOn F F' (inside C) (Plane.openSquare 0 1)) (hsub : 𝒜 ⊆ C) (hdense : C ⊆ closure 𝒜) (hcross : HasAnchorCrosscuts C 𝒜 u F) (hspoke : HasSpokes C 𝒜 u F) : IsHomeoOn (extendByBoundary C u F) (extendByBoundary modelCurve v F') (C ∪ inside C) (Plane.closedSquare 0 1)

thm:square-extension, for one curve. The glued map restricts to a homeomorphism of the closed Jordan domain onto the closed square, and extends u.

Continuity of the inverse is not proved directly: the domain is compact and the square is Hausdorff, so the continuous bijection Fbar is a closed map, which is exactly what continuousOn_iff_isClosed asks of the inverse.

The assembled hypothesis, and Schoenflies.SquareExtension

def Schoenflies.HasLimitHomeomorphism : Prop

Everything this section assumes, for every Jordan curve and every boundary homeomorphism onto the model square: a dense set of anchors, the limit homeomorphism of the interiors (prop:interior-homeomorphism), the anchor crosscuts with their target images (lem:skeleton-crosscuts and prop:skeleton-agreement), and the spokes at the anchors (lem:anchor-density).

Schoenflies.squareExtension_of_hasLimitHomeomorphism turns this into Schoenflies.SquareExtension, which is the input required by the final reduction.

Equations

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

theorem Schoenflies.squareExtension_of_hasLimitHomeomorphism (h : HasLimitHomeomorphism) : SquareExtension

thm:square-extension. Every homeomorphism of a Jordan curve onto the model square boundary extends to a homeomorphism of the closed Jordan domain onto the closed square.