feat: add NNReal.isOpen_Ico_zero (#15295)

Similar to the lemma `ENNReal.isOpen_Ico_zero` already in Mathlib. Co-authored-by: Rémy Degenne <[email protected]>
leanprover-community · Aug 15, 2024 · c66e20e · c66e20e
1 parent d49e552
commit c66e20e
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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