From a38feb832d9038498b98c521b8def028c97d74dc Mon Sep 17 00:00:00 2001
From: Jireh Loreaux <loreaujy@gmail.com>
Date: Tue, 27 Jun 2023 02:29:57 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20add=20`CompleteSpace`=20instance=20for?=
 =?UTF-8?q?=20`=E2=84=9D=E2=89=A50`=20(#5488)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mathlib/Topology/Instances/NNReal.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Topology/Instances/NNReal.lean b/Mathlib/Topology/Instances/NNReal.lean
index 55edb61c84cb8..b2945d62a85b6 100644
--- 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 _}