Commit 2026-04-28 19:12 defabb4c

View on Github →

chore(Topology/Order/SuccPred): use to_dual (#37781)

Estimated changes

Modified Mathlib/Order/Interval/Set/LinearOrder.lean

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem Order.Ioi_pred

deleted theorem Order.Ioi_pred_of_not_isMin

Modified Mathlib/Topology/Order/Basic.lean

Modified Mathlib/Topology/Order/SuccPred.lean

deleted theorem PredOrder.isOpen_iff

deleted theorem PredOrder.isOpen_singleton_iff

deleted theorem PredOrder.isPredLimit_of_mem_frontier

deleted theorem PredOrder.nhds_eq_pure