The one-point compactification of the real line as a Jordan curve

The real projective line, topologically the one-point compactification OnePoint ℝ, is a circle. This file records the resulting homeomorphism and the corresponding Jordan-curve fact. They let maps on the extended real boundary be treated using the Jordan-curve API. In particular, a proper injective parametrization by the real line extends to a continuous injection of OnePoint ℝ, so its image together with infinity is a Jordan curve in the one-point compactification of the ambient space.

The construction uses Mathlib's stereographic homeomorphism from the one-point compactification of a finite-dimensional real vector space to a sphere. The standard orthonormal basis ![1, Complex.I] then identifies the resulting two-dimensional Euclidean sphere with Circle.

Main definitions

• TauCeti.onePointRealHomeomorphCircle -- a homeomorphism from OnePoint ℝ to Circle.

Main results

• TauCeti.isJordanCurve_univ_onePoint_real -- the whole real projective line is a Jordan curve.
• TauCeti.isJordanCurve_insert_infty_range_of_isProperMap -- a proper simple real curve becomes a Jordan curve after adding the point at infinity.

noncomputable def TauCeti.onePointRealHomeomorphCircle : OnePoint ℝ ≃ₜ Circle

The one-point compactification of the real line is homeomorphic to the circle.

Mathlib's onePointEquivSphereOfFinrankEq realizes it as the unit sphere in two-dimensional Euclidean space. The standard orthonormal basis of ℂ carries that sphere isometrically onto the unit sphere in ℂ, which is definitionally Circle.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.isJordanCurve_univ_onePoint_real : IsJordanCurve Set.univ

The whole one-point compactification of the real line is a Jordan curve.

theorem TauCeti.isJordanCurve_insert_infty_range_of_isProperMap {X : Type u_1} [TopologicalSpace X] {f : ℝ → X} (hf : IsProperMap f) (hinj : Function.Injective f) : IsJordanCurve (insert OnePoint.infty (OnePoint.some '' Set.range f))

A proper injective parametrization by the real line becomes a Jordan curve in the one-point compactification of its ambient space. Both ends of the curve meet at infinity, and properness ensures continuity there.