Commit 2024-08-27 09:51 45e815c5

View on Github →

refactor(Order/SuccPred): Remove le_of_lt_succ and le_of_pred_lt from SuccOrder/PredOrder (#15881) See disccusion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/weaker.20SuccOrder.2FPredOrder

Estimated changes

modified theorem ENat.succ_def
modified theorem Order.le_of_lt_succ
modified theorem Order.le_of_pred_lt
added theorem Order.lt_succ_of_le
added theorem Order.pred_lt_of_le
added theorem Order.pred_lt_pred
added theorem Order.succ_lt_succ
modified def PredOrder.ofCore
modified theorem WithBot.pred_coe
deleted theorem WithBot.pred_coe_bot
modified theorem WithTop.succ_coe
deleted theorem WithTop.succ_coe_top
modified theorem Order.isPredLimitRecOn_pred
modified theorem Order.isSuccLimitRecOn_succ
modified theorem PredOrder.limitRecOn_pred
modified theorem SuccOrder.limitRecOn_succ