Theorem nhdsWithin_Iic_self_neBot

Modification history

2025-08-05 07:35
Mathlib/Topology/Order/LeftRight.lean
chore: further >6month old deprecations (#27799)
Deleted nhdsWithin_Iic_self_neBotView on Github โ†’
2024-12-23 08:37
Mathlib/Topology/Order/LeftRight.lean
chore(*): rename lemmas about `๐“[โ‰ฅ] a` etc (#20188) โ€ฆ
Added nhdsWithin_Iic_self_neBotView on Github โ†’
2023-10-30 03:09
Mathlib/Topology/Order/Basic.lean
feat: `โˆƒแถ  x in ๐“ a, x < a` (#7941) โ€ฆ
Deleted nhdsWithin_Iic_self_neBotView on Github โ†’
2023-02-05 17:41
Mathlib/Topology/Order/Basic.lean
feat: port Topology.Order.Basic (#2052)
Added nhdsWithin_Iic_self_neBotView on Github โ†’