Theorem eq_of_nhds_eq_nhds

Modification history

2024-03-16 17:36

Mathlib/Topology/Order.lean

feat: review and expand API on behavior of topological bases under some constructions (#10732) …

Deleted eq_of_nhds_eq_nhds View on Github →

2023-01-31 11:16

Mathlib/Topology/Order.lean

feat: port Topology.Order (#1843)

Added eq_of_nhds_eq_nhds View on Github →