Commit 2025-07-09 18:24 5c5a8deb

style(Mathlib/Topology): rename exterior (2/2) (#26919) This came to my attention while working on the proof that Alexandrov discrete spaces are locally path-connected. (#26492) In Mathlib, the intersection of all neighborhoods of a set s in a topological space is currently called exterior. However, for most mathematicians, the exterior of a set s refers to the complement of its closure (see here). This naming is very misleading, so exterior is clearly in need of renaming. The new name has been decided as neighborhoods kernel (nhdsKer), based on this Zulip thread.