The reals are complete #
This file provides the instances CompleteSpace ℝ
and CompleteSpace ℝ≥0
.
Along the way, we add a shortcut instance for the natural topology on ℝ≥0
(the one induced from ℝ
), and add some basic API.
Topology on ℝ≥0
#
All the instances are inherited from the corresponding structures on the reals.