The closed and open arcs of the circle

Mathlib's Circle.exp parametrizes the circle by angles. This file reads a closed arc Circle.exp '' Set.Icc a b off a subset of the circle and identifies its complement: a nonempty closed preconnected proper subset of the circle is such an arc, and the complement of a closed arc is the open arc Circle.exp '' Set.Ioo b (a + 2 * π) spanning the complementary angles.

Nothing here is specific to any curve theory; as with TauCeti/Topology/Circle/Metric.lean, these are facts about the model circle, and the transport of them to a Jordan curve — where a compact connected subset of the curve is thereby classified — is TauCeti/Topology/JordanCurve/Subcontinuum.lean.

The argument

The argument is the one for ℝ, run on a period of angles. Let T ⊆ Circle be closed, preconnected and not the whole circle, and pick z ∉ T. Cutting the circle at z — that is, reading it as Circle.exp on the period [t, t + 2π] for Circle.exp t = z — turns T into K = Circle.exp ⁻¹' T ∩ Icc t (t + 2 * π), a compact subset of ℝ avoiding both endpoints of that period, so K ⊆ Ioo t (t + 2 * π) and Circle.exp is injective on K. A continuous injection of a compact space into a Hausdorff one is a closed embedding (Continuous.isClosedEmbedding), hence inducing, and an inducing map reflects preconnectedness (Topology.IsInducing.isPreconnected_image), which carries preconnectedness of T = Circle.exp '' K back to K; a compact connected subset of ℝ is then a closed interval (eq_Icc_of_connected_compact). Hence T = Circle.exp '' Icc a b with b - a < 2 * π, the degenerate case a = b being a point.

The complement is read off the same period, moved to Ioc b (b + 2 * π) so that the closed arc becomes Icc (a + 2 * π) (b + 2 * π) and injectivity of Circle.exp applies to the difference.

Main results

• TauCeti.exists_eq_circleExp_image_Icc — a nonempty closed preconnected proper subset of the circle is Circle.exp '' Set.Icc a b for a pair of angles less than a full turn apart.
• TauCeti.compl_circleExp_image_Icc — the complement of such a closed arc is the open arc Circle.exp '' Set.Ioo b (a + 2 * π).

Both statements below are about a closed arc Circle.exp '' Set.Icc a b of angular width b - a less than a full turn. Nothing ties the angles to a period, so a consumer may translate them by any multiple of 2 * π.

theorem TauCeti.exists_eq_circleExp_image_Icc {T : Set Circle} (hT : IsClosed T) (hpre : IsPreconnected T) (hne : T.Nonempty) (hTuniv : T ≠ Set.univ) : ∃ (a : ℝ) (b : ℝ), a ≤ b ∧ b - a < 2 * Real.pi ∧ T = ⇑Circle.exp '' Set.Icc a b

A nonempty closed preconnected proper subset of the circle is a closed arc. The two angles are less than a full turn apart, so Circle.exp is injective on the interval carrying them, and the degenerate case a = b is a single point.

Closedness is what forces the arc to be closed: the set is compact, Circle being compact, and a compact connected subset of the line is a closed interval.

@[simp]

theorem TauCeti.compl_circleExp_image_Icc {a b : ℝ} (hab : a ≤ b) (hlt : b - a < 2 * Real.pi) : (⇑Circle.exp '' Set.Icc a b)ᶜ = ⇑Circle.exp '' Set.Ioo b (a + 2 * Real.pi)

The complement of a closed arc of the circle is the complementary open arc. The two arcs share their endpoints' angles: Circle.exp '' Set.Icc a b is complemented by Circle.exp '' Set.Ioo b (a + 2 * π), which is nonempty exactly because the closed arc is not the whole circle. Read left to right this removes a complement, so it is the normal form a consumer should reach for: simp [hab, hlt] rewrites with it.