Arcs and Jordan curves

A simple arc is the image of an injective continuous map from [0, 1]; a Jordan curve is the image of a map on [0, 1] which is injective before it returns to its start. Those are the blueprint's definitions verbatim.

The parameter domain is a subset of ℝ, not a type: an arc is carried by an ordinary f : ℝ → Plane together with ContinuousOn f unitInterval and InjOn f unitInterval. Mathlib's Path bundles a map out of ↥unitInterval instead, which is the right choice when paths are to be composed up to homotopy, and the wrong one here: subarcs are taken at arbitrary parameter pairs, reparametrisation is composition on ℝ with nothing to extract, and a Jordan curve's theorems are all about its parameters. Taking the circle as the domain would need a traversal of the circle by an interval, which is exactly what a trigonometry-free development does not have.

IsArcBetween is the set-level reading — an arc between two named points — and is the form most of the development speaks, since gluing and cutting are stated about endpoints.

Blueprint

• IsArc, IsJordanCurve — §1, the definitions of a simple arc and a Jordan curve.
• IsArcBetween — an arc between two named points.
• IsLoop — the parametrisation underlying a Jordan curve.

Arcs

def Schoenflies.IsArc (A : Set Plane) : Prop

A simple arc: the image of a continuous injective map on [0, 1].

Equations

• Schoenflies.IsArc A = ∃ (f : ℝ → Schoenflies.Plane), ContinuousOn f unitInterval ∧ Set.InjOn f unitInterval ∧ f '' unitInterval = A

def Schoenflies.IsArcBetween (A : Set Plane) (p q : Plane) : Prop

An arc between two named points: the set-level reading, and the form gluing and cutting are stated in.

Equations

• Schoenflies.IsArcBetween A p q = ∃ (f : ℝ → Schoenflies.Plane), ContinuousOn f unitInterval ∧ Set.InjOn f unitInterval ∧ f '' unitInterval = A ∧ f 0 = p ∧ f 1 = q

structure Schoenflies.IsLoop (f : ℝ → Plane) : Prop

A loop: continuous on [0, 1], returning to its start, and injective before it does.

• continuousOn : ContinuousOn f unitInterval
• closes : f 0 = f 1
• injOn : Set.InjOn f (Set.Ico 0 1)

def Schoenflies.IsJordanCurve (C : Set Plane) : Prop

A Jordan curve: the image of a loop.

Equations

• Schoenflies.IsJordanCurve C = ∃ (f : ℝ → Schoenflies.Plane), Schoenflies.IsLoop f ∧ f '' unitInterval = C

The unit interval, as a subset of ℝ

theorem Schoenflies.zero_mem_I : 0 ∈ unitInterval

theorem Schoenflies.one_mem_I : 1 ∈ unitInterval

theorem Schoenflies.isCompact_I : IsCompact unitInterval

theorem Schoenflies.isConnected_I : IsConnected unitInterval

theorem Schoenflies.isCompact_image_of_subset_I {f : ℝ → Plane} (hf : ContinuousOn f unitInterval) {S : Set ℝ} (hS : S ⊆ unitInterval) (hSc : IsClosed S) : IsCompact (f '' S)

The image of a relatively closed piece of the parameter interval is compact. This is what makes a parametrisation a closed map onto its arc, and hence its inverse continuous.

Elementary properties

theorem Schoenflies.IsArcBetween.isArc {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : IsArc A

theorem Schoenflies.IsArcBetween.left_mem {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : p ∈ A

theorem Schoenflies.IsArcBetween.right_mem {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : q ∈ A

theorem Schoenflies.IsArcBetween.reverse {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : IsArcBetween A q p

Running a piece the other way round.

theorem Schoenflies.IsArc.isCompact {A : Set Plane} (h : IsArc A) : IsCompact A

theorem Schoenflies.IsArc.isConnected {A : Set Plane} (h : IsArc A) : IsConnected A

theorem Schoenflies.IsArc.nonempty {A : Set Plane} (h : IsArc A) : A.Nonempty

theorem Schoenflies.IsArc.isClosed {A : Set Plane} (h : IsArc A) : IsClosed A

theorem Schoenflies.IsArc.exists_isArcBetween {A : Set Plane} (h : IsArc A) : ∃ (p : Plane) (q : Plane), IsArcBetween A p q

Every arc is an arc between its two endpoints.

theorem Schoenflies.IsJordanCurve.isCompact {C : Set Plane} (h : IsJordanCurve C) : IsCompact C

theorem Schoenflies.IsJordanCurve.isConnected {C : Set Plane} (h : IsJordanCurve C) : IsConnected C

theorem Schoenflies.IsJordanCurve.nonempty {C : Set Plane} (h : IsJordanCurve C) : C.Nonempty

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