Theorem eventually_nhdsWithin_pos_mem_Ioo

Modification history

2024-02-15 16:16
Mathlib/Topology/Order/Basic.lean
chore(Topology/Order): delete 2 lemmas (#10576) …
Deleted eventually_nhdsWithin_pos_mem_IooView on Github →
2023-02-05 17:41
Mathlib/Topology/Order/Basic.lean
feat: port Topology.Order.Basic (#2052)
Added eventually_nhdsWithin_pos_mem_IooView on Github →