Mathlib

The ordinary line has no ends. Compactify it by adding two points, −∞ and +∞.