Commit 2024-03-12 01:07 eb655f8b
View on Github →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".