Two points cut a Jordan curve into two arcs

Two distinct points of a Jordan curve cut it into two arcs between them, which cover the curve and meet in exactly those two points. This is the converse of IsJordanCurve.of_two_arcs, and the harder direction.

The whole argument is carried by the loop's parameters; the circle never appears. Pull the two points back to parameters s and t short of the finish — parameter_before_finish, which replaces a parameter at the finish by the start, the only use the closing condition gets — and order them, say s < t. Then the two pieces are what the loop makes of the parameters between s and t and of the parameters outside them:

• the middle piece f '' Icc s t is a subarc, produced by Subarc.lean's isArcBetween_subarc, whose injectivity hypothesis is confined to the traversed interval and so survives a loop;
• the outside piece f '' Icc 0 s ∪ f '' Icc t 1 is two end intervals glued where the loop closes up, produced by Concatenate.lean's IsArcBetween.concatenate.

That asymmetry — one subarc and one concatenation — is inherent to a parameter interval with a seam in it, and is not worth fighting. It costs one case split, at s = 0, where the front interval degenerates to a point that the back piece already carries at its far end.

Both halves of the conclusion are then facts about intervals of reals. Covering is the three-way split of [0,1] around two parameters, which is the linearity of the order and nothing else. Meeting is injectivity off the finish, applied on each of the three pieces; the one case that needs the loop rather than an arc is an outside parameter at the finish, which carries the same point as the start and so lands back on s.

Blueprint

• lem:jordan-circle — "any two distinct points of C divide it into two simple arcs having exactly those points in common". IsJordanCurve.two_arcs is that clause, proved directly from the parametrisation instead of through the model curve, so it does not wait on the loop-to-circle bridge.
• IsLoop.two_arcs_at_parameters — the parameter-level form the clause is assembled from.

Parameters short of the finish

A loop is injective on [0, 1) only, so every statement below has to keep its parameters away from 1. These two lemmas are the interface to that: one says injectivity holds as soon as neither parameter is the finish, the other says the finish can always be avoided.

theorem Schoenflies.IsLoop.injective_before_finish {f : ℝ → Plane} (hf : IsLoop f) {u v : ℝ} (hu : u ∈ unitInterval) (hv : v ∈ unitInterval) (hu1 : u ≠ 1) (hv1 : v ≠ 1) (h : f u = f v) : u = v

Two parameters short of the finish carrying the same point are equal. This is IsLoop.injOn with the half-open interval spelled as "in [0,1] and not 1", which is the form every use below produces.

theorem Schoenflies.IsLoop.parameter_before_finish {f : ℝ → Plane} (hf : IsLoop f) {p : Plane} (hp : p ∈ f '' unitInterval) : ∃ u ∈ unitInterval, u ≠ 1 ∧ f u = p

Every point of the curve has a parameter short of the finish. A parameter at the finish is replaced by the start, which carries the same point. This is the only use the closing condition gets.

theorem Schoenflies.IsLoop.finish_eq_start {f : ℝ → Plane} (hf : IsLoop f) : f 1 = f 0

The start and the finish are the same point of the curve; recorded in the direction the proofs below read it.

The three pieces of parameters

Two parameters s < t cut [0, 1] into the middle interval [s, t] and the two end intervals [0, s] and [t, 1]. Each piece needs the loop to be injective on its own parameters. On the middle and the front that is injectivity off the finish, since neither contains it; the back piece does contain the finish, and there the extra argument is that the only other parameter carrying f 1 is the start, which lies strictly before t.

theorem Schoenflies.IsLoop.front_subset_I {s : ℝ} (hs : s ∈ unitInterval) : Set.Icc 0 s ⊆ unitInterval

theorem Schoenflies.IsLoop.middle_subset_I {s t : ℝ} (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) : Set.Icc s t ⊆ unitInterval

theorem Schoenflies.IsLoop.back_subset_I {t : ℝ} (ht : t ∈ unitInterval) : Set.Icc t 1 ⊆ unitInterval

theorem Schoenflies.IsLoop.injective_on_front {f : ℝ → Plane} {s : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (hs1 : s ≠ 1) : Set.InjOn f (Set.Icc 0 s)

Injectivity on the front piece: no parameter of [0, s] is the finish, because s is not.

theorem Schoenflies.IsLoop.injective_on_middle {f : ℝ → Plane} {s t : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (ht1 : t ≠ 1) : Set.InjOn f (Set.Icc s t)

Injectivity on the middle piece: no parameter of [s, t] is the finish, because t is not.

theorem Schoenflies.IsLoop.back_at_finish {f : ℝ → Plane} {t : ℝ} (hf : IsLoop f) (ht : t ∈ unitInterval) (ht0 : 0 < t) {w : ℝ} (hw : w ∈ Set.Icc t 1) (h : f w = f 1) : w = 1

On the back piece the finish is the only parameter carrying f 1. A second one would be the start, by injectivity off the finish and the closing condition — but the start lies strictly before t.

theorem Schoenflies.IsLoop.injective_on_back {f : ℝ → Plane} {t : ℝ} (hf : IsLoop f) (ht : t ∈ unitInterval) (ht0 : 0 < t) : Set.InjOn f (Set.Icc t 1)

Injectivity on the back piece. Unlike the other two this piece contains the finish, so injectivity off the finish is not enough on its own; back_at_finish supplies the rest.

The three pieces are arcs

theorem Schoenflies.IsLoop.middle_IsArcBetween {f : ℝ → Plane} {s t : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (ht1 : t ≠ 1) (hst : s < t) : IsArcBetween (f '' Set.Icc s t) (f s) (f t)

The middle piece is an arc between the two cut points.

theorem Schoenflies.IsLoop.front_IsArcBetween {f : ℝ → Plane} {s : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (hs1 : s ≠ 1) (hs0 : 0 < s) : IsArcBetween (f '' Set.Icc 0 s) (f 0) (f s)

The front piece is an arc from the start to the first cut point.

theorem Schoenflies.IsLoop.back_IsArcBetween {f : ℝ → Plane} {t : ℝ} (hf : IsLoop f) (ht : t ∈ unitInterval) (ht1 : t ≠ 1) (ht0 : 0 < t) : IsArcBetween (f '' Set.Icc t 1) (f t) (f 1)

The back piece is an arc from the second cut point to the finish.

The outside piece

The parameters outside [s, t] are two intervals, glued at the point where the loop closes up: walk from t to the finish, then from the start to s. When s is the start the front interval degenerates to a single parameter, and the outside is the back piece alone — its far end already carries the point the front piece would have contributed.

theorem Schoenflies.IsLoop.back_meet_front {f : ℝ → Plane} {s t : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (hs1 : s ≠ 1) (hst : s < t) {z : Plane} (hzb : z ∈ f '' Set.Icc t 1) (hzf : z ∈ f '' Set.Icc 0 s) : z = f 1

The back and front pieces meet only where the loop closes up. A point on both comes from a parameter at or past t and from one at or before s; two distinct parameters short of the finish cannot carry the same point, and t ≤ s is false, so the back parameter is the finish.

theorem Schoenflies.IsLoop.outside_IsArcBetween {f : ℝ → Plane} {s t : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hst : s < t) : IsArcBetween (f '' Set.Icc 0 s ∪ f '' Set.Icc t 1) (f t) (f s)

The outside piece is an arc between the two cut points.

Covering, and where the pieces meet

theorem Schoenflies.IsLoop.parameters_split {s t : ℝ} (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) : unitInterval = Set.Icc s t ∪ (Set.Icc 0 s ∪ Set.Icc t 1)

The parameter interval splits three ways around any two of its points. Linearity of the order, and nothing else — the split does not even need the two points ordered, since when they are not the middle interval is empty and the two end intervals already overlap.

theorem Schoenflies.IsLoop.pieces_cover {f : ℝ → Plane} {s t : ℝ} (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) : f '' Set.Icc s t ∪ (f '' Set.Icc 0 s ∪ f '' Set.Icc t 1) = f '' unitInterval

The loop's images of the middle and of the outside cover the curve.

theorem Schoenflies.IsLoop.pieces_meet_at_ends {f : ℝ → Plane} {s t : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hst : s < t) : f '' Set.Icc s t ∩ (f '' Set.Icc 0 s ∪ f '' Set.Icc t 1) = {f s, f t}

The two pieces meet in exactly the two cut points.

Three cases, one for each way an outside parameter can be placed. The one that matters is the outside parameter being the finish: it carries the same point as the start, so the middle parameter is the start, which forces s to be it. That case is why the argument needs a loop rather than an arc.

The two arcs, at chosen parameters

theorem Schoenflies.IsLoop.two_arcs_at_parameters {f : ℝ → Plane} {s t : ℝ} (hf : IsLoop f) (hs : s ∈ unitInterval) (ht : t ∈ unitInterval) (hs1 : s ≠ 1) (ht1 : t ≠ 1) (hst : s < t) : ∃ (A : Set Plane) (B : Set Plane), IsArcBetween A (f s) (f t) ∧ IsArcBetween B (f t) (f s) ∧ A ∪ B = f '' unitInterval ∧ A ∩ B = {f s, f t}

Two parameters short of the finish cut the loop's image into two arcs between the points they carry, which cover it and meet in exactly those two points.

The pieces are named by the parameters, not chosen: the first is the middle interval's image, the second the outside's.

The theorem

theorem Schoenflies.IsJordanCurve.two_arcs {C : Set Plane} (hC : IsJordanCurve C) {p q : Plane} (hp : p ∈ C) (hq : q ∈ C) (hpq : p ≠ q) : ∃ (A : Set Plane) (B : Set Plane), IsArcBetween A p q ∧ IsArcBetween B p q ∧ A ∪ B = C ∧ A ∩ B = {p, q}

Two distinct points of a Jordan curve cut it into two arcs between them, which cover the curve and meet in exactly those two points.

The parameters carrying the two points come in one order or the other, and the conclusion is symmetric in the two pieces, so the second case is the first with the roles exchanged: the union and the intersection commute, and the unordered pair does too.

This is the exact converse of IsJordanCurve.of_two_arcs: that theorem's hypotheses are two arcs between the same two points meeting only there, which is what the two pieces produced here are — see IsJordanCurve.two_arcs_of_two_arcs.

theorem Schoenflies.IsJordanCurve.two_arcs_of_two_arcs {A B : Set Plane} {p q : Plane} (hA : IsArcBetween A p q) (hB : IsArcBetween B p q) (hmeet : A ∩ B = {p, q}) : IsJordanCurve (A ∪ B)

The composition check: the two arcs IsJordanCurve.two_arcs produces are exactly what IsJordanCurve.of_two_arcs consumes, and glue back to the curve one started from.