Gluing arcs

Two arcs meeting only at the endpoint they share glue to one arc; two arcs meeting at both of their ends glue to a Jordan curve. The glued parametrisation runs the first arc over the lower half of the parameter interval and the second over the upper half, each at double speed: t ↦ f (2 * t) below the midpoint and t ↦ g (2 * t - 1) above it. Since the parameter here is an honest real number, that is literally what the definition says.

The halves are [0, 1/2] and [1/2, 1]. They cover the interval, and each is closed, so continuity is Mathlib's pasting lemma ContinuousOn.union_of_isClosed. Injectivity splits four ways — both parameters below the midpoint, both above, and the two mixed orders — and only the mixed cases use the hypothesis that the two arcs meet nowhere else: there the common value lies on both arcs, hence is the shared endpoint, and each arc's own injectivity pins its parameter to the midpoint.

At the midpoint itself both branches of the if are meaningful and they agree, precisely because the first arc finishes where the second starts. That is what makes the glued map well defined rather than merely continuous, and it is why concatenate_upperHalf — the statement that the glued map is the retimed second arc on the whole closed upper half, midpoint included — carries the shared-endpoint hypothesis.

For the loop the seam analysis gains a second legitimate meeting point: besides the middle, where the arcs are glued, there are the outer ends, where the loop is allowed to repeat itself. Pinning those needs the start/finish counterparts of the midpoint lemmas.

Blueprint

• concatenate — §1, the glued parametrisation.
• IsArc.concatenate, IsArcBetween.concatenate — two arcs meeting only at the endpoint they share glue to an arc.
• IsLoop.concatenate — two arcs glued along both of their ends make a loop.
• IsJordanCurve.of_two_arcs — two arcs meeting exactly at their two shared endpoints make a Jordan curve; the converse of the two-arcs decomposition, and the form every construction of a curve takes.

The two halves of the parameter interval

def Schoenflies.lowerHalf : Set ℝ

The lower half of the parameter interval, where the first arc runs.

Equations

• Schoenflies.lowerHalf = Set.Icc 0 (1 / 2)

def Schoenflies.upperHalf : Set ℝ

The upper half of the parameter interval, where the second arc runs. The two halves overlap in the midpoint: that is the seam.

Equations

• Schoenflies.upperHalf = Set.Icc (1 / 2) 1

theorem Schoenflies.lowerHalf_subset_I : lowerHalf ⊆ unitInterval

theorem Schoenflies.upperHalf_subset_I : upperHalf ⊆ unitInterval

theorem Schoenflies.halves_union : lowerHalf ∪ upperHalf = unitInterval

theorem Schoenflies.isClosed_lowerHalf : IsClosed lowerHalf

theorem Schoenflies.isClosed_upperHalf : IsClosed upperHalf

theorem Schoenflies.double_mem_I {t : ℝ} (ht : t ∈ lowerHalf) : 2 * t ∈ unitInterval

Doubling a parameter below the midpoint reaches at most one.

theorem Schoenflies.doubleBack_mem_I {t : ℝ} (ht : t ∈ upperHalf) : 2 * t - 1 ∈ unitInterval

Doubling a parameter above the midpoint and stepping back reaches at least zero.

The glued parametrisation

noncomputable def Schoenflies.concatenate (f g : ℝ → Plane) : ℝ → Plane

Run f over the lower half of the interval and g over the upper half, each at double speed.

Equations

• Schoenflies.concatenate f g t = if t ≤ 1 / 2 then f (2 * t) else g (2 * t - 1)

theorem Schoenflies.concatenate_of_le {f g : ℝ → Plane} {t : ℝ} (ht : t ≤ 1 / 2) : concatenate f g t = f (2 * t)

theorem Schoenflies.concatenate_of_not_le {f g : ℝ → Plane} {t : ℝ} (ht : ¬t ≤ 1 / 2) : concatenate f g t = g (2 * t - 1)

theorem Schoenflies.concatenate_zero {f g : ℝ → Plane} : concatenate f g 0 = f 0

theorem Schoenflies.concatenate_one {f g : ℝ → Plane} : concatenate f g 1 = g 1

theorem Schoenflies.concatenate_upperHalf {f g : ℝ → Plane} (hmid : f 1 = g 0) {t : ℝ} (ht : t ∈ upperHalf) : concatenate f g t = g (2 * t - 1)

On the closed upper half the glued map is the retimed second arc — at the midpoint included, where the if still takes the first branch. The two branches agree there only because the first arc finishes where the second starts, which is what makes the glued map well defined.

Continuity

theorem Schoenflies.continuousOn_concatenate {f g : ℝ → Plane} (hf : ContinuousOn f unitInterval) (hg : ContinuousOn g unitInterval) (hmid : f 1 = g 0) : ContinuousOn (concatenate f g) unitInterval

Continuity of the glued map: each half carries a composition, and the halves are closed and cover.

Pinning a parameter at the seam

At a point where two of the pieces meet, the value is one of the shared points, and the injectivity of the arc it belongs to pins the parameter. Each half needs its own statement, since they retime differently; the loop needs the outer ends as well as the middle.

theorem Schoenflies.lowerHalf_at_finish {f : ℝ → Plane} (hfi : Set.InjOn f unitInterval) {t : ℝ} (ht : t ∈ lowerHalf) (h : f (2 * t) = f 1) : t = 1 / 2

theorem Schoenflies.lowerHalf_at_start {f : ℝ → Plane} (hfi : Set.InjOn f unitInterval) {t : ℝ} (ht : t ∈ lowerHalf) (h : f (2 * t) = f 0) : t = 0

theorem Schoenflies.upperHalf_at_start {g : ℝ → Plane} (hgi : Set.InjOn g unitInterval) {t : ℝ} (ht : t ∈ upperHalf) (h : g (2 * t - 1) = g 0) : t = 1 / 2

theorem Schoenflies.upperHalf_at_finish {g : ℝ → Plane} (hgi : Set.InjOn g unitInterval) {t : ℝ} (ht : t ∈ upperHalf) (h : g (2 * t - 1) = g 1) : t = 1

Injectivity

theorem Schoenflies.concatenate_seam {f g : ℝ → Plane} (hfi : Set.InjOn f unitInterval) (hgi : Set.InjOn g unitInterval) (hmid : f 1 = g 0) (hmeet : ∀ z ∈ f '' unitInterval, z ∈ g '' unitInterval → z = f 1) {x y : ℝ} (hx : x ∈ lowerHalf) (hy : y ∈ upperHalf) (h : concatenate f g x = concatenate f g y) : x = y

Across the seam: the common value lies on both arcs, so it is the shared endpoint, and each half's injectivity pins its own parameter to the midpoint. Stated for a parameter of each half rather than for x and y, so that the two orderings of the case split are the same theorem.

theorem Schoenflies.injOn_concatenate {f g : ℝ → Plane} (hfi : Set.InjOn f unitInterval) (hgi : Set.InjOn g unitInterval) (hmid : f 1 = g 0) (hmeet : ∀ z ∈ f '' unitInterval, z ∈ g '' unitInterval → z = f 1) : Set.InjOn (concatenate f g) unitInterval

Two arcs meeting only at the endpoint they share glue to an injective map.

What the glued map covers

theorem Schoenflies.image_concatenate {f g : ℝ → Plane} (hmid : f 1 = g 0) : concatenate f g '' unitInterval = f '' unitInterval ∪ g '' unitInterval

Each half retimes onto the whole interval, so the glued map's image is exactly the two arcs together.

The set-level gluing theorems

This is the form the rest of the development speaks: a piece is an arc between two named points, the parametrisations are chosen inside the proofs and never seen again.

theorem Schoenflies.IsArcBetween.concatenate {A B : Set Plane} {a b c : Plane} (hA : IsArcBetween A a b) (hB : IsArcBetween B b c) (hmeet : ∀ z ∈ A, z ∈ B → z = b) : IsArcBetween (A ∪ B) a c

Two pieces meeting only at the point where they are joined make one piece.

theorem Schoenflies.IsArc.concatenate {A B : Set Plane} {a b c : Plane} (hA : IsArcBetween A a b) (hB : IsArcBetween B b c) (hmeet : ∀ z ∈ A, z ∈ B → z = b) : IsArc (A ∪ B)

Two arcs meeting only at the endpoint they share glue to an arc.

Closing the loop

Two arcs that share both of their ends — the second runs back from where the first arrived to where it set out — glue to a loop rather than to an arc. Everything above carries over except the seam analysis: a common value now has two ways to be legitimate, at the middle where the arcs are glued and at the outer ends where the loop closes, and the second of those is exactly the repetition IsLoop allows itself at the finish.

theorem Schoenflies.concatenate_seam_loop {f g : ℝ → Plane} (hfi : Set.InjOn f unitInterval) (hgi : Set.InjOn g unitInterval) (hmid : f 1 = g 0) (hclose : g 1 = f 0) (hmeet : ∀ z ∈ f '' unitInterval, z ∈ g '' unitInterval → z = f 0 ∨ z = f 1) {x y : ℝ} (hx : x ∈ lowerHalf) (hy : y ∈ upperHalf) (hy1 : y ≠ 1) (h : concatenate f g x = concatenate f g y) : x = y

Across the seam, when the two arcs also share their outer ends. At the middle the argument is the one for arcs; at the outer ends the second arc is at its finish, so its parameter is 1 — which the hypothesis has excluded.

theorem Schoenflies.IsLoop.concatenate {f g : ℝ → Plane} (hfc : ContinuousOn f unitInterval) (hfi : Set.InjOn f unitInterval) (hgc : ContinuousOn g unitInterval) (hgi : Set.InjOn g unitInterval) (hmid : f 1 = g 0) (hclose : g 1 = f 0) (hmeet : ∀ z ∈ f '' unitInterval, z ∈ g '' unitInterval → z = f 0 ∨ z = f 1) : IsLoop (Schoenflies.concatenate f g)

Two arcs glued along both of their ends make a loop.

theorem Schoenflies.IsJordanCurve.of_two_arcs {A B : Set Plane} {a b : Plane} (hA : IsArcBetween A a b) (hB : IsArcBetween B b a) (hmeet : ∀ z ∈ A, z ∈ B → z = a ∨ z = b) : IsJordanCurve (A ∪ B)

Two pieces meeting exactly at their two shared endpoints make a Jordan curve. This is the converse of the two-arcs decomposition, and the form every construction of a curve takes: a cycle of a plane graph arrives as a path and one more edge back to where it started.