Separating curves, absorption, and the two cells of a crosscut

Definition 2.4 calls a Jordan curve separating when its complement has exactly two regions, one bounded and one unbounded, each with the curve as its boundary. Everything Part I proves about a polygonal curve and Part II proves about a general one is packaged in that single predicate, and the two lemmas below are the ones needed on both sides of the divide: they are proved from the definition alone.

The interface: inside and outside are total functions

The blueprint writes Int(C) and Ext(C) for the two regions and its consumers — the two crosscut theorems — name them in their statements. So the two regions must be functions of C, not sets produced by an existential inside the definition of separation. They are defined here for an arbitrary set: inside C is the union of the bounded components of the complement and outside C the union of the unbounded ones; together they partition Cᶜ. Separation is then the assertion that each of the two halves is one region with boundary C (Definition 2.4); that one is bounded and the other unbounded is then automatic, and so is "exactly two regions", since a connected clopen piece of Cᶜ is a component of it.

IsRegionOf C Ω says Ω is one of the two, and IsRegionPair C Ω Ω' that Ω, Ω' are the two in one order or the other. That is what lets Lemma 2.6 be stated once instead of twice: the blueprint's Ω is sometimes Int(C) and sometimes Ext(C), and every step of its proof is symmetric in that choice.

What the crosscut lemma actually needs

Lemma 2.6 is stated for a crosscut P of a separating curve C with arcs A₁, A₂, but its proof never uses that P and the Aᵢ are arcs, nor the endpoints p, q, nor even that C = A₁ ∪ A₂. What it uses is: Aᵢ ⊆ C, P ∩ C ⊆ Aᵢ (the crosscut meets the curve only in the shared endpoints, which lie on both arcs), Jᵢ = Aᵢ ∪ P separating, and A₁ ≠ A₂. The lemmas below are therefore stated at that level of generality, with arcs_ne supplying A₁ ≠ A₂ from the arc picture and isJordanCurve_union supplying the sentence "these are Jordan curves" from IsJordanCurve.of_two_arcs.

One further hypothesis of the blueprint is dropped: Ω is described there as the region containing P ∖ {p, q}, but what actually pins the roles of Ω, Ω†, Wᵢ and Vᵢ is the inclusion Ω† ⊆ Wᵢ, which is a hypothesis here. A consumer supplies it by IsSeparating.exists_isRegionPair_subset, which is the formal content of the blueprint's "being connected it lies in one region of ℝ² ∖ Jᵢ, so Wᵢ and Vᵢ are well defined".

Blueprint

• inside, outside, IsSeparating — Definition 2.4 (separating Jordan curve).
• IsSeparating.absorption — Lemma 2.5 (absorption).
• crosscut_cells — Lemma 2.6 (crosscut cells), all three parts, with the per-part lemmas cell_subset_region_diff, cell_isComponent, closure_cell_inter_curve stated separately because the bundled form carries the hypotheses of both indices at once.

The inside and the outside of a set

Both are defined for an arbitrary set, without any separation hypothesis: inside C collects the points whose component in the complement is bounded, outside C the rest of the complement.

def Schoenflies.inside (C : Set Plane) : Set Plane

The union of the bounded components of the complement — the blueprint's Int(C) once C is known to be separating.

Equations

• Schoenflies.inside C = {x : Schoenflies.Plane | x ∉ C ∧ Bornology.IsBounded (connectedComponentIn Cᶜ x)}

def Schoenflies.outside (C : Set Plane) : Set Plane

The union of the unbounded components of the complement — the blueprint's Ext(C) once C is known to be separating.

Equations

• Schoenflies.outside C = {x : Schoenflies.Plane | x ∉ C ∧ ¬Bornology.IsBounded (connectedComponentIn Cᶜ x)}

theorem Schoenflies.mem_inside_iff {C : Set Plane} {x : Plane} : x ∈ inside C ↔ x ∉ C ∧ Bornology.IsBounded (connectedComponentIn Cᶜ x)

theorem Schoenflies.mem_outside_iff {C : Set Plane} {x : Plane} : x ∈ outside C ↔ x ∉ C ∧ ¬Bornology.IsBounded (connectedComponentIn Cᶜ x)

theorem Schoenflies.inside_subset_compl {C : Set Plane} : inside C ⊆ Cᶜ

theorem Schoenflies.outside_subset_compl {C : Set Plane} : outside C ⊆ Cᶜ

theorem Schoenflies.inside_union_outside (C : Set Plane) : inside C ∪ outside C = Cᶜ

theorem Schoenflies.disjoint_inside_outside {C : Set Plane} : Disjoint (inside C) (outside C)

theorem Schoenflies.connectedComponentIn_subset_inside {C : Set Plane} {x : Plane} (hx : x ∈ inside C) : connectedComponentIn Cᶜ x ⊆ inside C

Boundedness of the component is constant along a component, so the inside is a union of whole components.

theorem Schoenflies.connectedComponentIn_subset_outside {C : Set Plane} {x : Plane} (hx : x ∈ outside C) : connectedComponentIn Cᶜ x ⊆ outside C

theorem Schoenflies.isOpen_inside {C : Set Plane} (hC : IsClosed C) : IsOpen (inside C)

A union of components of an open set is open.

theorem Schoenflies.isOpen_outside {C : Set Plane} (hC : IsClosed C) : IsOpen (outside C)

Definition 2.4: a separating Jordan curve

structure Schoenflies.IsSeparating (C : Set Plane) : Prop

Definition 2.4. A Jordan curve is separating when its complement has exactly two regions, one bounded and one unbounded, each with boundary C.

Since inside C and outside C always partition the complement into the bounded-component part and the unbounded-component part, "exactly two regions, one bounded and one unbounded" says precisely that each part is a single region; and the boundedness of one and unboundedness of the other are then consequences rather than hypotheses (IsSeparating.isBounded_inside, IsSeparating.not_isBounded_outside).

• isJordanCurve : IsJordanCurve C

  The set is a Jordan curve.

• isConnected_inside : IsConnected (inside C)

  The bounded part of the complement is a single region.

• isConnected_outside : IsConnected (outside C)

  The unbounded part of the complement is a single region.

• frontier_inside : frontier (inside C) = C

  The inside has the curve as its boundary.

• frontier_outside : frontier (outside C) = C

  The outside has the curve as its boundary.

theorem Schoenflies.IsSeparating.isClosed {C : Set Plane} (h : IsSeparating C) : IsClosed C

theorem Schoenflies.IsSeparating.isOpen_inside {C : Set Plane} (h : IsSeparating C) : IsOpen (inside C)

theorem Schoenflies.IsSeparating.isOpen_outside {C : Set Plane} (h : IsSeparating C) : IsOpen (outside C)

theorem Schoenflies.IsSeparating.isBounded_inside {C : Set Plane} (h : IsSeparating C) : Bornology.IsBounded (inside C)

The inside is bounded: it is connected and lies inside the complement, hence inside the component of any of its points, which is bounded by definition of inside.

theorem Schoenflies.IsSeparating.not_isBounded_outside {C : Set Plane} (h : IsSeparating C) : ¬Bornology.IsBounded (outside C)

The outside is unbounded: it contains an unbounded component.

theorem Schoenflies.IsSeparating.connectedComponentIn_eq_inside {C : Set Plane} {x : Plane} (h : IsSeparating C) (hx : x ∈ inside C) : connectedComponentIn Cᶜ x = inside C

The inside really is one region of the complement, that is, a connected component of it: it is a union of components which is itself connected. Together with its twin below this is the "exactly two regions" clause of Definition 2.4.

theorem Schoenflies.IsSeparating.connectedComponentIn_eq_outside {C : Set Plane} {x : Plane} (h : IsSeparating C) (hx : x ∈ outside C) : connectedComponentIn Cᶜ x = outside C

The outside is a connected component of the complement.

The two regions, named

IsRegionOf C Ω is "Ω is a region of ℝ² ∖ C" and IsRegionPair C Ω Ω' is "Ω and Ω' are the two regions". Both are stated without a separation hypothesis; the facts that make them useful carry one.

def Schoenflies.IsRegionOf (C Ω : Set Plane) : Prop

Ω is a region of the complement of C.

Equations

• Schoenflies.IsRegionOf C Ω = (Ω = Schoenflies.inside C ∨ Ω = Schoenflies.outside C)

def Schoenflies.IsRegionPair (C Ω Ω' : Set Plane) : Prop

Ω and Ω' are the two regions of the complement of C, in one order or the other.

Equations

• Schoenflies.IsRegionPair C Ω Ω' = (Ω = Schoenflies.inside C ∧ Ω' = Schoenflies.outside C ∨ Ω = Schoenflies.outside C ∧ Ω' = Schoenflies.inside C)

theorem Schoenflies.IsSeparating.isRegionOf_connectedComponentIn {C : Set Plane} {x : Plane} (h : IsSeparating C) (hx : x ∉ C) : IsRegionOf C (connectedComponentIn Cᶜ x)

Every component of the complement is one of the two regions: there are no others. This is the last clause of "exactly two regions".

theorem Schoenflies.IsRegionOf.inside (C : Set Plane) : IsRegionOf C (Schoenflies.inside C)

theorem Schoenflies.IsRegionOf.outside (C : Set Plane) : IsRegionOf C (Schoenflies.outside C)

theorem Schoenflies.IsRegionOf.subset_compl {C Ω : Set Plane} (h : IsRegionOf C Ω) : Ω ⊆ Cᶜ

theorem Schoenflies.IsRegionOf.isOpen {C Ω : Set Plane} (h : IsRegionOf C Ω) (hC : IsSeparating C) : IsOpen Ω

theorem Schoenflies.IsRegionOf.isConnected {C Ω : Set Plane} (h : IsRegionOf C Ω) (hC : IsSeparating C) : IsConnected Ω

theorem Schoenflies.IsRegionOf.connectedComponentIn_eq {C Ω : Set Plane} {x : Plane} (h : IsRegionOf C Ω) (hC : IsSeparating C) (hx : x ∈ Ω) : connectedComponentIn Cᶜ x = Ω

A region is a connected component of the complement.

theorem Schoenflies.IsRegionOf.frontier_eq {C Ω : Set Plane} (h : IsRegionOf C Ω) (hC : IsSeparating C) : frontier Ω = C

theorem Schoenflies.IsRegionOf.subset_closure {C Ω : Set Plane} (h : IsRegionOf C Ω) (hC : IsSeparating C) : C ⊆ closure Ω

Every point of the curve is a limit of points of the region: this is the half of frontier Ω = C that absorption uses.

theorem Schoenflies.IsRegionOf.closure_eq {C Ω : Set Plane} (h : IsRegionOf C Ω) (hC : IsSeparating C) : closure Ω = Ω ∪ C

The closure of a region is the region together with the curve.

theorem Schoenflies.IsRegionPair.left {C Ω Ω' : Set Plane} (h : IsRegionPair C Ω Ω') : IsRegionOf C Ω

theorem Schoenflies.IsRegionPair.right {C Ω Ω' : Set Plane} (h : IsRegionPair C Ω Ω') : IsRegionOf C Ω'

theorem Schoenflies.IsRegionPair.symm {C Ω Ω' : Set Plane} (h : IsRegionPair C Ω Ω') : IsRegionPair C Ω' Ω

theorem Schoenflies.IsRegionPair.union_eq {C Ω Ω' : Set Plane} (h : IsRegionPair C Ω Ω') : Ω ∪ Ω' = Cᶜ

theorem Schoenflies.IsRegionPair.disjoint {C Ω Ω' : Set Plane} (h : IsRegionPair C Ω Ω') : Disjoint Ω Ω'

theorem Schoenflies.IsRegionPair.subset_left_of_isPreconnected {C Ω Ω' : Set Plane} (h : IsRegionPair C Ω Ω') (hC : IsSeparating C) {S : Set Plane} (hS : IsPreconnected S) (hne : S.Nonempty) (hSC : S ⊆ Cᶜ) (hSΩ' : Disjoint S Ω') : S ⊆ Ω

A connected set off the curve and off one region lies in the other. This is the only place where "exactly two regions" is used, and it is used in exactly that form.

theorem Schoenflies.IsSeparating.exists_isRegionPair_subset {C : Set Plane} (hC : IsSeparating C) {S : Set Plane} (hS : IsPreconnected S) (hne : S.Nonempty) (hSC : Disjoint S C) : ∃ (W : Set Plane) (V : Set Plane), IsRegionPair C W V ∧ S ⊆ W

A nonempty connected set disjoint from the curve lies in one of the two regions. This is the well-definedness clause of Lemma 2.6: "being connected it lies in one region of ℝ² ∖ Jᵢ, so Wᵢ and Vᵢ are well defined".

Lemma 2.5: absorption

theorem Schoenflies.absorption_of_subset_closure {C J Ω V : Set Plane} (hCΩ : C ⊆ closure Ω) (hV : IsOpen V) (hfr : frontier V ⊆ J) (hsub : Ω ⊆ V) : C \ J ⊆ V

Lemma 2.5 (absorption), set-theoretic core. If every point of C is a limit of points of Ω, and Ω sits inside an open V whose frontier lies in J, then C misses V only where J does.

theorem Schoenflies.IsSeparating.absorption {C J Ω V : Set Plane} (hC : IsSeparating C) (hJ : IsSeparating J) (hΩ : IsRegionOf C Ω) (hV : IsRegionOf J V) (hsub : Ω ⊆ V) : C \ J ⊆ V

Lemma 2.5 (absorption). If a region Ω of the complement of a separating curve C is contained in a region V of the complement of a separating curve J, then all of C off J lies in V.

Lemma 2.6: the two cells of a crosscut

The setting: C is a separating curve, Ω and Ω' its two regions, J a separating curve with P ⊆ J ⊆ C ∪ P, and W, V the two regions of ℝ² ∖ J, with Ω' ⊆ W. The blueprint's J is Aᵢ ∪ P for one of the two arcs Aᵢ; the proof only needs the two inclusions.

theorem Schoenflies.disjoint_cell_curve {C J Ω' W V : Set Plane} (hC : IsSeparating C) (hJ : IsSeparating J) (hΩ' : IsRegionOf C Ω') (hWV : IsRegionPair J W V) (hΩW : Ω' ⊆ W) : Disjoint V C

The far region Ω' absorbs all of C off J, so the near cell V misses C entirely: the part of C off J is in W, and the part on J is off V because V misses J.

theorem Schoenflies.cell_subset_region_diff {C J P Ω Ω' W V : Set Plane} (hC : IsSeparating C) (hJ : IsSeparating J) (hΩ : IsRegionPair C Ω Ω') (hWV : IsRegionPair J W V) (hΩW : Ω' ⊆ W) (hPJ : P ⊆ J) : V ⊆ Ω \ P

Lemma 2.6, first half of (a): the cell V is contained in Ω ∖ P. It misses C, it is connected, and it misses Ω' because Ω' ⊆ W; so it lies in Ω. It misses P because it misses J ⊇ P.

theorem Schoenflies.cell_isComponent {C J P Ω Ω' W V : Set Plane} (hC : IsSeparating C) (hJ : IsSeparating J) (hΩ : IsRegionPair C Ω Ω') (hWV : IsRegionPair J W V) (hΩW : Ω' ⊆ W) (hPJ : P ⊆ J) (hJCP : J ⊆ C ∪ P) (z : Plane) : z ∈ V → connectedComponentIn (Ω \ P) z = V

Lemma 2.6 (a): the cell V is a connected component of Ω ∖ P. Its frontier is J, which lies in C ∪ P and so misses the open set Ω ∖ P; Lemma 1.7 does the rest.

theorem Schoenflies.closure_cell_inter_curve {C J Ω' W V : Set Plane} (hC : IsSeparating C) (hJ : IsSeparating J) (hΩ' : IsRegionOf C Ω') (hWV : IsRegionPair J W V) (hΩW : Ω' ⊆ W) : closure V ∩ C = J ∩ C

Lemma 2.6 (c): the closure of the cell meets C exactly in J ∩ C. The closure is V ∪ J, and V misses C.

The arc-level side conditions

Two small facts turn the blueprint's arc picture into the hypotheses the lemmas above take.

theorem Schoenflies.isJordanCurve_union {P A : Set Plane} {p q : Plane} (hA : IsArcBetween A p q) (hP : IsArcBetween P p q) (hmeet : ∀ z ∈ A, z ∈ P → z = p ∨ z = q) : IsJordanCurve (A ∪ P)

The two curves of Lemma 2.6 are Jordan curves: an arc from p to q and a second arc from p to q meeting it only at those two points glue to a Jordan curve.

theorem Schoenflies.arcs_ne {A₁ A₂ : Set Plane} {p q : Plane} (hmeet : A₁ ∩ A₂ ⊆ {p, q}) (hA : ¬A₁ ⊆ {p, q}) : A₁ ≠ A₂

Lemma 2.6 (b), arc side: the two arcs of C from p to q are distinct, because they meet only at p and q while neither is just {p, q}.

Lemma 2.6, bundled

theorem Schoenflies.crosscut_cells {C P A₁ A₂ Ω Ω' : Set Plane} (hC : IsSeparating C) (hJ₁ : IsSeparating (A₁ ∪ P)) (hJ₂ : IsSeparating (A₂ ∪ P)) (hA₁ : A₁ ⊆ C) (hA₂ : A₂ ⊆ C) (hP₁ : P ∩ C ⊆ A₁) (hP₂ : P ∩ C ⊆ A₂) (hne : A₁ ≠ A₂) (hΩ : IsRegionPair C Ω Ω') {W₁ V₁ W₂ V₂ : Set Plane} (hWV₁ : IsRegionPair (A₁ ∪ P) W₁ V₁) (hΩW₁ : Ω' ⊆ W₁) (hWV₂ : IsRegionPair (A₂ ∪ P) W₂ V₂) (hΩW₂ : Ω' ⊆ W₂) : (V₁ ⊆ Ω \ P ∧ ∀ z ∈ V₁, connectedComponentIn (Ω \ P) z = V₁) ∧ (V₂ ⊆ Ω \ P ∧ ∀ z ∈ V₂, connectedComponentIn (Ω \ P) z = V₂) ∧ V₁ ≠ V₂ ∧ closure V₁ ∩ C = A₁ ∧ closure V₂ ∩ C = A₂

Lemma 2.6 (crosscut cells). Let C be a separating curve with regions Ω and Ω', let A₁, A₂ ⊆ C be the two arcs cut out by a crosscut P which meets C only in points of both arcs, and suppose the two curves Jᵢ = Aᵢ ∪ P are separating. Let Wᵢ be the region of ℝ² ∖ Jᵢ containing Ω' and Vᵢ the other one. Then

• (a) each Vᵢ is a connected component of Ω ∖ P;
• (b) V₁ ≠ V₂;
• (c) closure Vᵢ ∩ C = Aᵢ.

The blueprint proves (b) from the boundaries; here it falls straight out of (c), since V₁ = V₂ would make A₁ = A₂.