Two points cut a Jordan curve into two arcs

Removing one point from a Jordan curve leaves a path-connected set; removing two leaves exactly two pieces. This file proves both, first for the model curve Circle and then for an arbitrary Jordan curve by transport along the homeomorphism that TauCeti.IsJordanCurve provides.

The argument on the circle

Both circle statements come straight out of Mathlib's arc API. For one point, Circle.isPathConnected_compl_singleton is exactly the statement, and is used directly. For two distinct points z and w, Mathlib parametrizes the two arcs they determine by the paths Circle.path z w and Circle.path w z, and records that the two ranges meet exactly in {z, w} (Circle.range_path_inter_range_path) and that each open arc is the complement of the opposite closed one (Circle.compl_range_path). So the two open arcs are complements of compact sets, hence open, and they are path connected as continuous images of the interval Set.Ioo 0 1; openness is what makes the pair a genuine separation rather than merely a partition.

Why this is a layer-L5 prerequisite

Layer L5 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) is Carathéodory's boundary correspondence, and the injectivity half of its hard direction argues by contradiction: if the continuous extension of a Riemann map identified two distinct points of the bounding circle, those two points would cut the circle into two arcs, and the geometry of the image would force the extension to be constant on one of them — which TauCeti.not_eqOn_const_inter_sphere_of_injOn in TauCeti/Analysis/Complex/Conformal/ArcConstancy.lean rules out. That file records the missing input explicitly: "two identified boundary points cut the circle into two arcs" is a statement about the curve, not about the map. Mathlib cuts the circle; what this file adds is the same cutting for an arbitrary Jordan curve, which is the generality the argument needs, since it applies the cutting to frontier Ω — a Jordan curve, not a circle — on the image side.

Generality

The Jordan-curve statements are for a subset of an arbitrary topological space, as in TauCeti/Topology/JordanCurve/Basic.lean; no separation axiom is needed, because the curve carries the subspace topology of a space homeomorphic to the circle and every hypothesis is checked there. The corollaries for a circle Metric.sphere c r of ℂ are the case the conformal layers consume.

Main results

• TauCeti.IsJordanCurve.isPathConnected_sdiff_singleton — a Jordan curve minus a point is path connected; for a point of the curve it is an open arc — homeomorphic to a punctured circle, not to a closed interval — and in particular one point never separates the curve.
• TauCeti.exists_isOpen_isPathConnected_union_eq_compl_pair_circle — two distinct points cut the circle into two disjoint nonempty open path-connected arcs.
• TauCeti.IsJordanCurve.exists_isPathConnected_union_eq_sdiff_pair — the same for an arbitrary Jordan curve, together with the statement that the two arcs are its connected components: every preconnected subset of the cut curve lies in one of them.
• TauCeti.IsJordanCurve.not_isPreconnected_sdiff_pair — consequently two points always separate a Jordan curve.
• TauCeti.isPathConnected_sphere_sdiff_singleton, TauCeti.exists_isPathConnected_union_eq_sphere_sdiff_pair and TauCeti.not_isPreconnected_sphere_sdiff_pair — the three statements for a circle of ℂ, the form in which the bounding circle of a disc is cut.

References

• Ch. Pommerenke, Boundary Behaviour of Conformal Maps, Ch. 2.
• C. Carathéodory, Über die gegenseitige Beziehung der Ränder bei der konformen Abbildung, Math. Ann. 73 (1913).

Cutting the circle

theorem TauCeti.exists_isOpen_isPathConnected_union_eq_compl_pair_circle {z w : Circle} (hzw : z ≠ w) : ∃ (A : Set Circle) (B : Set Circle), IsOpen A ∧ IsOpen B ∧ IsPathConnected A ∧ IsPathConnected B ∧ Disjoint A B ∧ A ∪ B = {z, w}ᶜ

Two distinct points cut the circle into two arcs. The complement of {z, w} is the union of two disjoint nonempty open path-connected sets, namely the two open arcs Circle.path z w '' Ioo 0 1 and Circle.path w z '' Ioo 0 1 that Mathlib cuts the circle into.

Openness is the substantive part: it says the two arcs are a separation of {z, w}ᶜ, so that no connected subset of the cut circle can meet both, which is how the pair is used. Each open arc is the complement of the opposite closed arc by Circle.compl_range_path, hence open because a range of a path is compact; and the two closed arcs meet in {z, w} by Circle.range_path_inter_range_path, which is the union statement.

Cutting a Jordan curve

Both statements below are the circle statement carried across the parametrization TauCeti.jordanParam e of a Jordan curve by the circle, whose properties — continuity, injectivity, range, and that it is inducing — are in TauCeti/Topology/JordanCurve/Basic.lean.

theorem TauCeti.IsJordanCurve.isPathConnected_sdiff_singleton {X : Type u_1} [TopologicalSpace X] {C : Set X} (h : IsJordanCurve C) (p : X) : IsPathConnected (C \ {p})

A Jordan curve minus a point is path connected, being homeomorphic to the circle minus a point (Circle.isPathConnected_compl_singleton). So a Jordan curve is not separated by any one of its points; it takes two, by TauCeti.IsJordanCurve.not_isPreconnected_sdiff_pair. The point need not lie on the curve: removing one that does not leaves the curve itself.

theorem TauCeti.IsJordanCurve.exists_isPathConnected_union_eq_sdiff_pair {X : Type u_1} [TopologicalSpace X] {C : Set X} {p q : X} (h : IsJordanCurve C) (hp : p ∈ C) (hq : q ∈ C) (hpq : p ≠ q) : ∃ (A : Set X) (B : Set X), IsPathConnected A ∧ IsPathConnected B ∧ Disjoint A B ∧ A ∪ B = C \ {p, q} ∧ ∀ ⦃S : Set X⦄, S ⊆ C \ {p, q} → IsPreconnected S → S ⊆ A ∨ S ⊆ B

Two distinct points cut a Jordan curve into two arcs. For p ≠ q on a Jordan curve C there are two disjoint path-connected sets A and B with A ∪ B = C \ {p, q}, and they are the connected components of the cut curve: every preconnected subset of C \ {p, q} lies inside one of them.

The last clause is what makes the pair canonical, and is the form the Carathéodory boundary argument uses: a connected set that avoids p and q cannot get from one arc to the other. It comes from openness of the two arcs of the circle in TauCeti.exists_isOpen_isPathConnected_union_eq_compl_pair_circle, transported along the parametrization, which is an inducing map, so preconnectedness may be tested upstairs.

theorem TauCeti.IsJordanCurve.not_isPreconnected_sdiff_pair {X : Type u_1} [TopologicalSpace X] {C : Set X} {p q : X} (h : IsJordanCurve C) (hp : p ∈ C) (hq : q ∈ C) (hpq : p ≠ q) : ¬IsPreconnected (C \ {p, q})

Two points separate a Jordan curve. Removing two distinct points from a Jordan curve leaves a set that is not preconnected: it splits into the two arcs of TauCeti.IsJordanCurve.exists_isPathConnected_union_eq_sdiff_pair, each of which is nonempty, and a preconnected set lying in one of them cannot contain the other.

The circles of ℂ

theorem TauCeti.isPathConnected_sphere_sdiff_singleton {r : ℝ} (c : ℂ) (hr : 0 < r) (z : ℂ) : IsPathConnected (Metric.sphere c r \ {z})

A circle of ℂ minus a point is path connected, being a Jordan curve (TauCeti.isJordanCurve_sphere). This is the boundary circle of a disc with one boundary point removed, the set the Carathéodory boundary argument works on; the removed point need not lie on the circle.

theorem TauCeti.exists_isPathConnected_union_eq_sphere_sdiff_pair {r : ℝ} (c : ℂ) {z w : ℂ} (hz : z ∈ Metric.sphere c r) (hw : w ∈ Metric.sphere c r) (hzw : z ≠ w) : ∃ (A : Set ℂ) (B : Set ℂ), IsPathConnected A ∧ IsPathConnected B ∧ Disjoint A B ∧ A ∪ B = Metric.sphere c r \ {z, w} ∧ ∀ ⦃S : Set ℂ⦄, S ⊆ Metric.sphere c r \ {z, w} → IsPreconnected S → S ⊆ A ∨ S ⊆ B

Two points cut a circle of ℂ into two arcs. This is TauCeti.IsJordanCurve.exists_isPathConnected_union_eq_sdiff_pair for the bounding circle of a disc, which is the curve the Carathéodory boundary argument cuts: a connected set of boundary points avoiding z and w lies in one of the two arcs they determine.

No positivity hypothesis on r is needed: two distinct points of Metric.sphere c r already force 0 < r.

theorem TauCeti.not_isPreconnected_sphere_sdiff_pair {r : ℝ} (c : ℂ) {z w : ℂ} (hz : z ∈ Metric.sphere c r) (hw : w ∈ Metric.sphere c r) (hzw : z ≠ w) : ¬IsPreconnected (Metric.sphere c r \ {z, w})

Two points separate a circle of ℂ: removing two distinct points of Metric.sphere c r leaves a set that is not preconnected. As above, 0 < r follows from the two points being distinct.