From c66e20ecff7734236437c9298384e2e6a4aa34c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9my=20Degenne?= <Remydegenne@gmail.com>
Date: Thu, 15 Aug 2024 09:43:32 +0000
Subject: [PATCH] feat: add NNReal.isOpen_Ico_zero (#15295)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Similar to the lemma `ENNReal.isOpen_Ico_zero` already in Mathlib.



Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
---
 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 e12bda18c19cc..f7759c47f7eea 100644
--- a/Mathlib/Topology/Instances/NNReal.lean
+++ b/Mathlib/Topology/Instances/NNReal.lean
@@ -75,6 +75,9 @@ instance : ContinuousStar ℝ≥0 where
   continuous_star := continuous_id
 section coe
 
+lemma isOpen_Ico_zero {x : NNReal} : IsOpen (Set.Ico 0 x) :=
+  Ico_bot (a := x) ▸ isOpen_Iio
+
 variable {α : Type*}
 
 open Filter Finset