Theorem SuccOrder.isOpen_singleton_of_not_isSuccPrelimit

Modification history

2026-02-13 02:37
Mathlib/Topology/Order/SuccPred.lean
feat: order topologies of successor orders (#32455)
Added SuccOrder.isOpen_singleton_of_not_isSuccPrelimitView on Github →