Commit 2026-03-05 10:25 faa2693e

View on Github →

chore(Order/SuccPred/Limit): use to_dual on everything that was missing (#35639)

Estimated changes

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Order/Bounds/Basic.lean

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem IsGLB.isPredLimit_of_notMem

deleted theorem IsGLB.isPredPrelimit_of_notMem

deleted theorem IsGLB.mem_of_not_isPredLimit

deleted theorem IsGLB.mem_of_not_isPredPrelimit

deleted theorem Order.IsPredLimit.isGLB_Ioi

deleted theorem Order.IsPredLimit.le_iff_forall_le

deleted theorem Order.IsPredLimit.lt_iff_exists_lt

deleted theorem Order.IsPredLimit.nonempty_Ioi

deleted theorem Order.IsPredPrelimit.isGLB_Ioi

deleted theorem Order.IsPredPrelimit.isMax_of_noMin

deleted theorem Order.IsPredPrelimit.le_iff_forall_le

deleted theorem Order.IsPredPrelimit.lt_iff_exists_lt

deleted theorem Order.isGLB_Ioi_iff_isPredPrelimit

deleted theorem Order.isPredLimit_toDual_iff

deleted theorem Order.isPredPrelimit_iff

deleted theorem Order.isPredPrelimit_iff_of_noMin

deleted theorem Order.not_isPredLimit

deleted theorem Order.not_isPredLimit_of_noMin

modified theorem Order.not_isPredLimit_of_not_isPredPrelimit

deleted theorem Order.not_isPredPrelimit

deleted theorem Order.not_isPredPrelimit_of_noMin