Theorem Set.ordConnectedComponent_mem_nhds

Modification history

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