Theorem nhds_nhdsAdjoint_of_ne

Modification history

2024-02-14 01:35
Mathlib/Topology/Order.lean
refactor(WithZeroTopology): use `nhdsAdjoint` (#10411) …
Added nhds_nhdsAdjoint_of_neView on Github →