Theorem nhdsWithin_Iic_neBot

Modification history

2026-03-05 12:46

Mathlib/Topology/Order/LeftRight.lean

chore(Topology/Order/LeftRight): use `to_dual` (#35637) …

Deleted nhdsWithin_Iic_neBot View on Github →

2023-10-30 03:09

Mathlib/Topology/Algebra/Order/LeftRight.lean

feat: `∃ᶠ x in 𝓝 a, x < a` (#7941) …

Modified nhdsWithin_Iic_neBot View on Github →

2023-02-05 17:41

Mathlib/Topology/Order/Basic.lean

feat: port Topology.Order.Basic (#2052)

Added nhdsWithin_Iic_neBot View on Github →