Mathlib

Atlas/Foundations/Extended number systems

One-point compactification

1/4

The extended line has two ends. Identify +∞ with −∞ and you get a circle.