Theorem nhdsWithin_Ici_self_neBot

Modification history

2023-10-30 03:09
Mathlib/Topology/Order/Basic.lean
feat: `โˆƒแถ  x in ๐“ a, x < a` (#7941) โ€ฆ
Deleted nhdsWithin_Ici_self_neBotView on Github โ†’
2023-02-05 17:41
Mathlib/Topology/Order/Basic.lean
feat: port Topology.Order.Basic (#2052)
Added nhdsWithin_Ici_self_neBotView on Github โ†’