Theorem PredOrder.isOpen_singleton_of_not_isPredPrelimit

Modification history

2026-04-08 16:40
Mathlib/Topology/Order/SuccPred.lean
chore: remove unneeded `to_dual existing` (#37778) …
Deleted PredOrder.isOpen_singleton_of_not_isPredPrelimitView on Github →
2026-02-13 02:37
Mathlib/Topology/Order/SuccPred.lean
feat: order topologies of successor orders (#32455)
Added PredOrder.isOpen_singleton_of_not_isPredPrelimitView on Github →