Theorem eventually_nhdsWithin_eventually_nhds_iff_of_isOpen

Modification history

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