Theorem eventually_nhdsNE_eventually_nhds_iff

Modification history

2025-12-10 06:35
Mathlib/Topology/Separation/Basic.lean
feat: derivatives of meromorphic functions are meromorphic (#32385) …
Added eventually_nhdsNE_eventually_nhds_iffView on Github →