Commit 2023-06-23 06:08 50226ad0

View on Github →

feat(Topology/Separation): add eventually_ne_nhds and eventually_ne_nhdsWithin (#5412)

Estimated changes

Modified Mathlib/Topology/Separation.lean

added theorem eventually_ne_nhds

added theorem eventually_ne_nhdsWithin