Subarcs, open arcs, and the subarc basis

A subarc is the arc restricted to a subinterval of the parameter interval — but an arc is carried by a map on [0, 1], so the restriction has to be reparametrised back onto it. That reparametrisation is reparam a b : t ↦ a + t * (b - a): pure arithmetic, with no inverse to construct and no choice to make. With it a subarc is a composition, and the two things an arc must be — continuous and injective — are the two things a composition inherits.

Injectivity is required only on uIcc a b, the parameter interval actually traversed, not on all of [0, 1]. That is what lets the two arcs of a Jordan curve be cut out of a loop, whose parametrisation is injective on [0, 1) only.

The substance of the file is the last two sections. A parametrisation is an open map onto its arc: the image of a relatively open piece of the parameter interval is relatively open in the arc. This is where the continuity of the inverse earns its keep, and it is proved without ever constructing that inverse — a continuous injection on a compact set is a closed map onto its image, and a closed injective map is open onto its image, by complements. Together with basic_piece_inside_ball, which puts such a piece inside any prescribed ball, these images are a basis of the arc's subspace topology.

Relative openness is stated in the ambient form ∃ V, IsOpen V ∧ W = V ∩ A rather than through the subtype ↥A, since every consumer here works with subsets of the plane.

Blueprint

The blueprint uses subarcs throughout §1 without a numbered statement of their own; they are the tool behind, among others, the model-curve parametrization (lem:jordan-circle), where "the relatively open subarcs of C" are exactly the images produced by image_isRelOpen, and the density arguments of lem:accessible-dense, which need basic_piece_inside_ball.

• subarc, isArcBetween_subarc — a piece of an arc is again an arc.
• IsArc.exists_isArcBetween_subset — the set-level reading: two points of an arc bound a subarc of it.
• openArc — the blueprint's P°, an arc without its two endpoints.
• image_isRelOpen — a parametrisation is an open map onto its arc; openArc_isRelOpen and openArc_subarc_isRelOpen are the "relatively open subarcs" of lem:jordan-circle.
• basic_piece_inside_ball — the subarc basis.

Reparametrising [0, 1] onto a subinterval

def Schoenflies.reparam (a b : ℝ) : ℝ → ℝ

The affine map carrying [0, 1] onto the parameter interval between a and b, running from a to b.

Equations

• Schoenflies.reparam a b t = a + t * (b - a)

@[simp]

theorem Schoenflies.reparam_zero {a b : ℝ} : reparam a b 0 = a

@[simp]

theorem Schoenflies.reparam_one {a b : ℝ} : reparam a b 1 = b

theorem Schoenflies.continuous_reparam {a b : ℝ} : Continuous (reparam a b)

theorem Schoenflies.reparam_injective {a b : ℝ} (hab : a ≠ b) : Function.Injective (reparam a b)

The reparametrisation is injective as soon as it is not constant.

theorem Schoenflies.image_reparam_I {a b : ℝ} : reparam a b '' unitInterval = Set.uIcc a b

reparam a b carries the unit interval exactly onto uIcc a b. This is segment_eq_image' read through the identification of a real segment with an unordered closed interval.

theorem Schoenflies.mapsTo_reparam {a b : ℝ} : Set.MapsTo (reparam a b) unitInterval (Set.uIcc a b)

theorem Schoenflies.uIcc_subset_I {a b : ℝ} (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) : Set.uIcc a b ⊆ unitInterval

A subinterval of the unit interval stays inside it: uIcc is the convex hull of its two endpoints, and the unit interval is convex.

Subarcs

def Schoenflies.subarc (f : ℝ → Plane) (a b : ℝ) : ℝ → Plane

The subarc of f between the parameters a and b: the arc traversed from f a to f b, reparametrised so that it is again a map on [0, 1].

Equations

• Schoenflies.subarc f a b t = f (Schoenflies.reparam a b t)

@[simp]

theorem Schoenflies.subarc_zero {a b : ℝ} {f : ℝ → Plane} : subarc f a b 0 = f a

@[simp]

theorem Schoenflies.subarc_one {a b : ℝ} {f : ℝ → Plane} : subarc f a b 1 = f b

theorem Schoenflies.subarc_image {a b : ℝ} {f : ℝ → Plane} : subarc f a b '' unitInterval = f '' Set.uIcc a b

The image of a subarc is the arc restricted to the subinterval — which is what "sub" means, and the form every consumer wants.

theorem Schoenflies.subarc_image_subset {a b : ℝ} {f : ℝ → Plane} (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) : subarc f a b '' unitInterval ⊆ f '' unitInterval

theorem Schoenflies.continuousOn_subarc {a b : ℝ} {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) : ContinuousOn (subarc f a b) unitInterval

theorem Schoenflies.injOn_subarc {a b : ℝ} {f : ℝ → Plane} (hi : Set.InjOn f (Set.uIcc a b)) (hab : a ≠ b) : Set.InjOn (subarc f a b) unitInterval

Injectivity of the subarc needs injectivity of f only where the subarc runs.

theorem Schoenflies.isArcBetween_subarc {a b : ℝ} {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f (Set.uIcc a b)) (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) (hab : a ≠ b) : IsArcBetween (f '' Set.uIcc a b) (f a) (f b)

A subarc between two distinct parameters is an arc between the two values there. The injectivity hypothesis is confined to the traversed interval, so this applies to a piece of a Jordan curve as well as to a piece of an arc.

theorem Schoenflies.isArc_subarc {a b : ℝ} {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f (Set.uIcc a b)) (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) (hab : a ≠ b) : IsArc (f '' Set.uIcc a b)

theorem Schoenflies.isArcBetween_subarc_of_injOn_I {a b : ℝ} {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f unitInterval) (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) (hab : a ≠ b) : IsArcBetween (f '' Set.uIcc a b) (f a) (f b)

The version for an arc, whose parametrisation is injective everywhere.

theorem Schoenflies.IsArc.exists_isArcBetween_subset {A : Set Plane} (h : IsArc A) {p q : Plane} (hp : p ∈ A) (hq : q ∈ A) (hpq : p ≠ q) : ∃ B ⊆ A, IsArcBetween B p q

Any two distinct points of an arc are the endpoints of a subarc of it. The set-level form, for the consumers that never see a parametrisation.

The arc without its endpoints

def Schoenflies.openArc (f : ℝ → Plane) : Set Plane

The open arc — the blueprint's P°: an arc with its two endpoints removed.

Taken on the parameter side, as the image of the open unit interval, because that is the form the subarc basis argument needs: an open subarc is the image of an open subinterval. Injectivity then says it is also the arc minus the two endpoint values, which is how the blueprint reads it (openArc_eq_diff).

Equations

• Schoenflies.openArc f = f '' Set.Ioo 0 1

theorem Schoenflies.Ioo_subset_I : Set.Ioo 0 1 ⊆ unitInterval

theorem Schoenflies.openArc_subset {f : ℝ → Plane} : openArc f ⊆ f '' unitInterval

theorem Schoenflies.openArc_eq_diff {f : ℝ → Plane} (hi : Set.InjOn f unitInterval) : openArc f = f '' unitInterval \ {f 0, f 1}

On an arc the two readings of "without its endpoints" agree: dropping the endpoints of the parameter interval drops exactly the two endpoint values, since injectivity means no other parameter shares them.

theorem Schoenflies.openArc_subarc {a b : ℝ} {f : ℝ → Plane} (hab : a ≠ b) : openArc (subarc f a b) = f '' Set.uIoo a b

The open arc of a subarc is the arc restricted to the open subinterval.

The interior of an arc, set-level

openArc is stated for a parametrisation. Three separate modules needed the same facts stated for the set — IsArcBetween A p q gives A ∖ {p, q} connected, nonempty, and having both endpoints in its closure — and each proved them again from scratch, one of them twice under two names. Two of those copies were literally the same statement in modules that do not import each other, so the build never noticed: alpha-equivalent Props are defeq under proof irrelevance, and Lean's import checker accepts them. They live here now.

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

The two ends of an arc are distinct: they are the images of 0 and 1.

theorem Schoenflies.IsArcBetween.diff_eq_openArc {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : ∃ (f : ℝ → Plane), ContinuousOn f unitInterval ∧ A \ {p, q} = f '' Set.Ioo 0 1

The interior of an arc is the image of the open parameter interval. The bridge from IsArcBetween, which is about the set, to openArc, which is about a parametrisation.

theorem Schoenflies.IsArcBetween.isPreconnected_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : IsPreconnected (A \ {p, q})

The interior of an arc is connected. It is the continuous image of Ioo 0 1.

theorem Schoenflies.IsArcBetween.nonempty_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : (A \ {p, q}).Nonempty

The interior of an arc is nonempty: Ioo 0 1 is.

theorem Schoenflies.IsArcBetween.isConnected_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : IsConnected (A \ {p, q})

The interior of an arc is connected in the nonempty sense.

theorem Schoenflies.IsArcBetween.left_mem_closure_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : p ∈ closure (A \ {p, q})

An endpoint of an arc is a limit of its interior. This is what turns "the closure of a cell meets the curve in one arc only" into a statement about the endpoints of a crosscut, and it is what says an ear's two ends lie on the boundary of the face its interior lies in.

theorem Schoenflies.IsArcBetween.right_mem_closure_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : q ∈ closure (A \ {p, q})

theorem Schoenflies.IsArcBetween.closure_diff {A : Set Plane} {p q : Plane} (h : IsArcBetween A p q) : closure (A \ {p, q}) = A

An arc is the closure of its interior. The arc is compact, hence closed, so the closure of the interior is inside it; conversely the interior is inside its own closure and each of the two endpoints is a limit of it.

A parametrisation is an open map onto its arc

theorem Schoenflies.image_isRelOpen {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f unitInterval) {U : Set ℝ} (hU : IsOpen U) : ∃ (V : Set Plane), IsOpen V ∧ f '' (U ∩ unitInterval) = V ∩ f '' unitInterval

The parametrisation is an open map onto its arc. The image of a relatively open piece of the parameter interval is relatively open in the arc.

No inverse is constructed. The complement piece I \ U is compact, so its image is compact, so it is closed; and by injectivity the image of U ∩ I is exactly the arc minus that closed set. Stated for a relatively open piece U ∩ I rather than for a subarc, because at an endpoint the basic neighbourhood is half-open — openArc of a subarc is the interior case, and this covers both.

theorem Schoenflies.exists_ball_inter_subset_image {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f unitInterval) {U : Set ℝ} (hU : IsOpen U) {x : Plane} (hx : x ∈ f '' (U ∩ unitInterval)) : ∃ ε > 0, Metric.ball x ε ∩ f '' unitInterval ⊆ f '' (U ∩ unitInterval)

The pointwise reading of the previous theorem, and the one consumers use: around every point of the image of a relatively open piece there is a ball meeting the arc only inside that image. This is precisely the continuity of the inverse parametrisation.

theorem Schoenflies.openArc_isRelOpen {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f unitInterval) : ∃ (V : Set Plane), IsOpen V ∧ openArc f = V ∩ f '' unitInterval

The open arc is relatively open in the arc: the blueprint's P° is a relatively open subarc.

theorem Schoenflies.openArc_subarc_isRelOpen {a b : ℝ} {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) (hi : Set.InjOn f unitInterval) (ha : a ∈ unitInterval) (hb : b ∈ unitInterval) : ∃ (V : Set Plane), IsOpen V ∧ f '' Set.uIoo a b = V ∩ f '' unitInterval

A subarc without its endpoints is relatively open in the arc. These are the "relatively open subarcs" the blueprint speaks of.

The subarc basis

theorem Schoenflies.basic_piece_inside_ball {f : ℝ → Plane} (hc : ContinuousOn f unitInterval) {x : Plane} (hx : x ∈ f '' unitInterval) {r : ℝ} (hr : 0 < r) : ∃ (c : ℝ) (d : ℝ), x ∈ f '' (Set.Ioo c d ∩ unitInterval) ∧ f '' (Set.Ioo c d ∩ unitInterval) ⊆ Metric.ball x r

Every neighbourhood of a point of the arc contains the image of an open subinterval around its parameter. With image_isRelOpen, which says those images are relatively open, this makes them a basis of the arc's subspace topology.

The piece is the parameter interval cut by an interval around the parameter, which is half-open exactly when the point is an endpoint.