Theorem Set.ordT5Nhd_mem_nhdsSet

Modification history

2023-02-06 15:54
Mathlib/Topology/Algebra/Order/T5.lean
feat: port Topology.Algebra.Order.T5 (#2102)
Added Set.ordT5Nhd_mem_nhdsSetView on Github →