feat: @[simp] Icc a b ∈ 𝓝 x (#11178)

Currently doesn't simplify since `interior_Icc` goes the other way.

We were using it in PrimeNumberTheoremAnd for things like "point does not lie on boundary of rectangle".




Co-authored-by: L Lllvvuu <git@llllvvuu.dev>

Author: llllvvuu

Mathlib/Topology/Order/Basic.lean

@@ -1542,16 +1542,29 @@ theorem interior_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} : interior (Icc
   rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]
 #align interior_Icc interior_Icc
 
+@[simp]
+theorem Icc_mem_nhds_iff [NoMinOrder α] [NoMaxOrder α] {a b x : α} :
+    Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
+  rw [← interior_Icc, mem_interior_iff_mem_nhds]
+
 @[simp]
 theorem interior_Ico [NoMinOrder α] {a b : α} : interior (Ico a b) = Ioo a b := by
   rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
 #align interior_Ico interior_Ico
 
+@[simp]
+theorem Ico_mem_nhds_iff [NoMinOrder α] {a b x : α} : Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
+  rw [← interior_Ico, mem_interior_iff_mem_nhds]
+
 @[simp]
 theorem interior_Ioc [NoMaxOrder α] {a b : α} : interior (Ioc a b) = Ioo a b := by
   rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
 #align interior_Ioc interior_Ioc
 
+@[simp]
+theorem Ioc_mem_nhds_iff [NoMaxOrder α] {a b x : α} : Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b := by
+  rw [← interior_Ioc, mem_interior_iff_mem_nhds]
+
 theorem closure_interior_Icc {a b : α} (h : a ≠ b) : closure (interior (Icc a b)) = Icc a b :=
   (closure_minimal interior_subset isClosed_Icc).antisymm <|
     calc