feat: add CompleteSpace instance for ℝ≥0 (#5488)

leanprover-community · Jun 27, 2023 · a38feb8 · a38feb8
1 parent 3c3631e
commit a38feb8
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/Topology/Instances/NNReal.lean b/Mathlib/Topology/Instances/NNReal.lean
@@ -74,6 +74,9 @@ instance : SecondCountableTopology ℝ≥0 :=
 instance : OrderTopology ℝ≥0 :=
   orderTopology_of_ordConnected (t := Ici 0)
 
+instance : CompleteSpace ℝ≥0 :=
+  isClosed_Ici.completeSpace_coe
+
 section coe
 
 variable {α : Type _}