Commit 2026-02-13 02:37 80dbc510

View on Github →

feat: order topologies of successor orders (#32455)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Cover.lean

added theorem CovBy.Ioo_eq_Ico

added theorem CovBy.Ioo_eq_Ioc

Modified Mathlib/SetTheory/Ordinal/Topology.lean

modified theorem Ordinal.isOpen_iff

modified theorem Ordinal.isOpen_singleton_iff

modified theorem Ordinal.isSuccLimit_of_mem_frontier

Created Mathlib/Topology/Order/SuccPred.lean

added theorem PredOrder.isOpen_iff

added theorem PredOrder.isOpen_singleton_iff

added theorem PredOrder.isOpen_singleton_of_not_isPredPrelimit

added theorem PredOrder.isPredLimit_of_mem_frontier

added theorem PredOrder.nhds_eq_pure

added theorem SuccOrder.isOpen_iff

added theorem SuccOrder.isOpen_singleton_iff

added theorem SuccOrder.isOpen_singleton_of_not_isSuccPrelimit

added theorem SuccOrder.isSuccLimit_of_mem_frontier

added theorem SuccOrder.nhds_eq_pure