A Jordan curve separates the plane

Half of the Jordan curve theorem: the complement of a Jordan curve C is disconnected. The proof is the blueprint's — build a subdivision of K(3,3) out of the curve, a chord of it, a detour above it, and a connecting arc, and appeal to Graph.IsArcK33.elim.

The configuration

Fix a coordinate i in which C has nonzero width, and let j be the other one. Write m and M for the extreme i-coordinates on C, and let p₁, p₂ be the points of C on the two supporting lines {z | z i = m}, {z | z i = M} with the largest j-coordinate. Two points of a Jordan curve cut it into two arcs C₁, C₂ (IsJordanCurve.two_arcs). Both meet the middle line {z | z i = (m + M) / 2}, by the intermediate value theorem; a closest pair a ∈ C₁, b ∈ C₂ on that line spans a segment L₄ whose interior misses C. Running up the two supporting lines and across above the curve gives a polygonal set meeting C exactly in {p₁, p₂} and missing L₄; a simple arc L₅ inside it (exists_simple_poly_of_poly) is the blueprint's detour.

The blueprint argues inside the unbounded component: it supposes L₄ \ {a, b} to lie there, and concludes that it does not. Here the contradiction hypothesis is the statement being negated — that the whole complement is preconnected — which is weaker to assume and gives the same K(3,3). Nothing about the unbounded component is needed, so nothing about it is proved; exists_unique_unbounded_connectedComponentIn_compl at the end is the separate cheap fact.

If the complement were preconnected, a simple polygonal arc R inside it would join an interior point of L₄ to an interior point of L₅. Its last parameter on L₄ and the first one after that on L₅ cut out a piece L₆ meeting L₄ ∪ L₅ only at its two ends — this is why the blueprint takes such care over the order in which c' and d' are chosen. Cutting C₁ at a, C₂ at b, L₅ at the far end d' of L₆ and L₄ at its near end c' produces nine arcs on the six points {p₁, p₂, c'}, {a, b, d'}, meeting only where a K(3,3) forces them to. That is impossible, so the complement is not preconnected.

Coordinates instead of a rotation

The blueprint rotates so that the direction of nonzero width becomes horizontal. Here the two coordinate indices are carried as parameters i ≠ j of not_isPreconnected_compl_of_coord instead, and the headline theorem picks whichever pair works. No rotation, no trigonometry and no coordinate-swap symmetry lemma is needed: every step is symmetric in the two indices except for which one is named.

The blueprint's opening step — a Jordan curve is not contained in a line — is not needed in this form. All it is used for is a direction of nonzero width, and that follows from the curve having two distinct points (IsJordanCurve.exists_ne). The degenerate configurations the blueprint's step rules out are excluded downstream instead, by C₁ ∩ C₂ = {p₁, p₂}.

Blueprint

• Schoenflies.not_isPreconnected_compl_of_coord, Schoenflies.IsJordanCurve.not_isPreconnected_compl, Schoenflies.IsJordanCurve.exists_connectedComponentIn_ne — prop:jordan-disconnected.
• Schoenflies.exists_unique_unbounded_connectedComponentIn_compl — the opening sentence of the blueprint's Jordan section: the complement of a compact set has exactly one unbounded component.
• Graph.isArcK33_of_pieces — the packaging of cor:k33-subdivision (through Graph.IsArcK33.elim) that this configuration fits.
• Schoenflies.IsArcBetween.exists_split — an arc cut at an interior point; the arc analogue of the second clause of lem:jordan-circle, which Schoenflies.IsJordanCurve.two_arcs is.

For the integrator

Three groups of declarations here are general and have no home yet on main:

• Schoenflies.Plane.coord_ext, axisVec, setCoord, coord_eq_of_mem_segment, le_coord_of_mem_segment, coord_le_of_mem_segment belong beside the coordinate half-planes in Schoenflies/Square.lean.
• Schoenflies.IsArcBetween.exists_split belongs in Schoenflies/Subarc.lean, next to IsArc.exists_isArcBetween_subset; Schoenflies.injective_three is a Fin 3 triviality.
• Graph.isArcK33_of_pieces belongs in Schoenflies/Graph/K33Planar.lean, next to Graph.IsArcK33.

theorem Schoenflies.Plane.coord_ext {i j : Fin 2} (hij : i ≠ j) {z w : Plane} (hi : z.ofLp i = w.ofLp i) (hj : z.ofLp j = w.ofLp j) : z = w

Two points of the plane agreeing in two distinct coordinates are equal.

noncomputable def Schoenflies.Plane.axisVec (j : Fin 2) : Plane

The unit vector along the coordinate axis j.

Equations

• Schoenflies.Plane.axisVec j = Schoenflies.Plane.mk (if j = 0 then 1 else 0) (if j = 1 then 1 else 0)

@[simp]

theorem Schoenflies.Plane.axisVec_self (j : Fin 2) : (axisVec j).ofLp j = 1

theorem Schoenflies.Plane.axisVec_of_ne {i j : Fin 2} (h : i ≠ j) : (axisVec j).ofLp i = 0

noncomputable def Schoenflies.Plane.setCoord (z : Plane) (j : Fin 2) (t : ℝ) : Plane

The point obtained from z by moving its j-th coordinate to t and leaving the other coordinate where it was. This is how the two upper corners of the polygonal detour above the curve are named without committing to which of the two coordinates is the horizontal one.

Equations

• z.setCoord j t = z + (t - z.ofLp j) • Schoenflies.Plane.axisVec j

@[simp]

theorem Schoenflies.Plane.setCoord_self (z : Plane) (j : Fin 2) (t : ℝ) : (z.setCoord j t).ofLp j = t

theorem Schoenflies.Plane.setCoord_of_ne {i j : Fin 2} (h : i ≠ j) (z : Plane) (t : ℝ) : (z.setCoord j t).ofLp i = z.ofLp i

Coordinates along a segment

theorem Schoenflies.Plane.coord_eq_of_mem_segment {k : Fin 2} {r : ℝ} {s t z : Plane} (hs : s.ofLp k = r) (ht : t.ofLp k = r) (hz : z ∈ segment ℝ s t) : z.ofLp k = r

A coordinate constant at both ends of a segment is constant along it.

theorem Schoenflies.Plane.le_coord_of_mem_segment {k : Fin 2} {r : ℝ} {s t z : Plane} (hs : r ≤ s.ofLp k) (ht : r ≤ t.ofLp k) (hz : z ∈ segment ℝ s t) : r ≤ z.ofLp k

A lower bound on a coordinate at both ends of a segment holds along it.

theorem Schoenflies.Plane.coord_le_of_mem_segment {k : Fin 2} {r : ℝ} {s t z : Plane} (hs : s.ofLp k ≤ r) (ht : t.ofLp k ≤ r) (hz : z ∈ segment ℝ s t) : z.ofLp k ≤ r

An upper bound on a coordinate at both ends of a segment holds along it.

theorem Schoenflies.injective_three {α : Type u_1} {a b c : α} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : Function.Injective ![a, b, c]

Injectivity of a three-element vector, from the three distinctness facts.

Cutting an arc at an interior point

theorem Schoenflies.IsArcBetween.exists_split {A : Set Plane} {p q z : Plane} (h : IsArcBetween A p q) (hz : z ∈ A) (hzp : z ≠ p) (hzq : z ≠ q) : ∃ (A₁ : Set Plane) (A₂ : Set Plane), IsArcBetween A₁ p z ∧ IsArcBetween A₂ z q ∧ A₁ ∪ A₂ = A ∧ A₁ ∩ A₂ = {z}

An arc splits at any of its interior points into two arcs which cover it and meet exactly there. This is the arc analogue of IsJordanCurve.two_arcs, and is what turns each branch of the configuration below into two branch paths of the K(3,3).

theorem Graph.isArcK33_of_pieces {x y : Fin 3 → Schoenflies.Plane} {P : Fin 3 → Fin 3 → Set Schoenflies.Plane} {Ch Sg : Fin 3 → Set Schoenflies.Plane} (harc : ∀ (i j : Fin 3), Schoenflies.IsArcBetween (P i j) (x i) (y j)) (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i j : Fin 3), x i ≠ y j) (hsubCh₀ : ∀ (j : Fin 3), P 0 j ⊆ Ch j) (hsubCh₁ : ∀ (j : Fin 3), P 1 j ⊆ Ch j) (hsubSg : ∀ (j : Fin 3), P 2 j ⊆ Sg j) (hsplit : ∀ (j : Fin 3), P 0 j ∩ P 1 j ⊆ {y j}) (hChCh : ∀ (j l : Fin 3), j ≠ l → Ch j ∩ Ch l ⊆ {x 0, x 1}) (hChSg : ∀ (j l : Fin 3), Ch j ∩ Sg l ⊆ {y j}) (hSgSg : ∀ (j l : Fin 3), j ≠ l → P 2 j ∩ P 2 l ⊆ {x 2}) : IsArcK33 x y P

Nine arcs assembled from three chains, two bridges of a fourth, and a ninth arc.

This is a packaging lemma: it repackages the meet clause of Graph.IsArcK33 as the five containment facts that a K(3,3) subdivision found inside a plane configuration actually produces. The rows 0 and 1 of P are the two halves of three chains Ch 0, Ch 1, Ch 2 running from x 0 to x 1, each cut at the point y j; row 2 holds three further pieces, carried by sets Sg j, that all issue from x 2.

The hypotheses are exactly what the separation proof below has to hand, and nothing about their geometry is used: only the listed intersections.

The separation proof

theorem Schoenflies.not_isPreconnected_of_arc_chord_detour {C C₁ C₂ L₅ : Set Plane} {p₁ p₂ a b : Plane} (hCopen : IsOpen Cᶜ) (harc₁ : IsArcBetween C₁ p₁ p₂) (harc₂ : IsArcBetween C₂ p₁ p₂) (hL₅arc : IsArcBetween L₅ p₁ p₂) (hcover : C₁ ∪ C₂ = C) (hCmeet : C₁ ∩ C₂ = {p₁, p₂}) (haC₁ : a ∈ C₁) (hbC₂ : b ∈ C₂) (ha_ne : a ≠ p₁ ∧ a ≠ p₂) (hb_ne : b ≠ p₁ ∧ b ≠ p₂) (hab_ne : a ≠ b) (hopenSeg : ∀ z ∈ openSegment ℝ a b, z ∉ C) (hL₅C : ∀ z ∈ L₅, z ∈ C → z = p₁ ∨ z = p₂) (hL₅L₄ : ∀ z ∈ L₅, z ∉ segment ℝ a b) : ¬IsPreconnected Cᶜ

A chord and an exterior detour across the two arcs force a planar K(3,3) configuration if the complement were connected.

theorem Schoenflies.not_isPreconnected_compl_of_coord {C : Set Plane} (hC : IsJordanCurve C) {i j : Fin 2} (hij : i ≠ j) {u v : Plane} (hu : u ∈ C) (hv : v ∈ C) (huv : u.ofLp i ≠ v.ofLp i) : ¬IsPreconnected Cᶜ

Proposition 3.2 (a Jordan curve separates), with the coordinate direction named.

i is the blueprint's horizontal direction and j its vertical one; the hypothesis on u and v is that the projection of C to the i-th coordinate has nonzero width, which is all the blueprint's rotation achieves. IsJordanCurve.not_isPreconnected_compl discharges it.

The headline

theorem Schoenflies.IsJordanCurve.exists_ne {C : Set Plane} (hC : IsJordanCurve C) : ∃ u ∈ C, ∃ v ∈ C, u ≠ v

A Jordan curve carries two distinct points: the loop parametrising it is injective on [0, 1), which has two distinct points.

theorem Schoenflies.IsJordanCurve.not_isPreconnected_compl {C : Set Plane} (hC : IsJordanCurve C) : ¬IsPreconnected Cᶜ

Proposition 3.2 (a Jordan curve separates the plane). The complement of a Jordan curve is not preconnected.

The direction hypothesis of not_isPreconnected_compl_of_coord is discharged here: the curve has two distinct points, so they differ in one of the two coordinates, and that coordinate plays the role of the blueprint's horizontal one. No rotation is performed — the proof is run for whichever coordinate projection has nonzero width, with the two coordinate indices carried as parameters.

theorem Schoenflies.IsJordanCurve.exists_connectedComponentIn_ne {C : Set Plane} (hC : IsJordanCurve C) : ∃ u ∈ Cᶜ, ∃ v ∈ Cᶜ, connectedComponentIn Cᶜ u ≠ connectedComponentIn Cᶜ v

Proposition 3.2, in the form the Jordan curve theorem consumes: the complement of a Jordan curve has at least two connected components. Stated as two of its points lying in different components, since that is what thm:jordan starts from.

It is genuinely the same statement: a set all of whose points share one component is that component, and a component is preconnected.

The unbounded component

Cheap, and what thm:jordan needs to name the exterior: a compact set sits inside a square, the outside of that square is connected and misses it, so the whole outside lies in one component of the complement — the only unbounded one.

theorem Schoenflies.exists_unique_unbounded_connectedComponentIn_compl {C : Set Plane} (hC : IsCompact C) : ∃ base ∈ Cᶜ, ¬Bornology.IsBounded (connectedComponentIn Cᶜ base) ∧ ∀ z ∈ Cᶜ, ¬Bornology.IsBounded (connectedComponentIn Cᶜ z) → connectedComponentIn Cᶜ z = connectedComponentIn Cᶜ base

The unbounded component of the complement of a compact set. It exists, it swallows the outside of any square containing the set, and it is the only unbounded component.