Commit 2024-09-16 17:23 7f6525c6

View on Github →

feat(Order/SuccPred/Limit): induction principles for IsSuccLimit and IsPredLimit (#16719)

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.isPredLimitRecOn_of_isMax

added theorem Order.isPredLimitRecOn_of_isPredLimit

added theorem Order.isPredLimitRecOn_pred

added theorem Order.isPredLimitRecOn_pred_of_not_isMin

deleted theorem Order.isPredPrelimitRecOn_limit

added theorem Order.isPredPrelimitRecOn_of_isPredPrelimit

deleted theorem Order.isPredPrelimitRecOn_pred'

added theorem Order.isPredPrelimitRecOn_pred_of_not_isMin

added theorem Order.isSuccLimitRecOn_of_isMin

added theorem Order.isSuccLimitRecOn_of_isSuccLimit

added theorem Order.isSuccLimitRecOn_succ

added theorem Order.isSuccLimitRecOn_succ_of_not_isMax

deleted theorem Order.isSuccPrelimitRecOn_limit

added theorem Order.isSuccPrelimitRecOn_of_isSuccPrelimit

deleted theorem Order.isSuccPrelimitRecOn_succ'

added theorem Order.isSuccPrelimitRecOn_succ_of_not_isMax

added theorem PredOrder.limitRecOn_isMax

added theorem PredOrder.limitRecOn_of_isPredLimit

added theorem PredOrder.limitRecOn_pred

added theorem PredOrder.limitRecOn_pred_of_not_isMin

deleted theorem PredOrder.prelimitRecOn_limit

added theorem PredOrder.prelimitRecOn_of_isPredPrelimit

deleted theorem PredOrder.prelimitRecOn_pred'

added theorem PredOrder.prelimitRecOn_pred_of_not_isMin

added theorem SuccOrder.limitRecOn_isMin

added theorem SuccOrder.limitRecOn_of_isSuccLimit

added theorem SuccOrder.limitRecOn_succ

added theorem SuccOrder.limitRecOn_succ_of_not_isMax

deleted theorem SuccOrder.prelimitRecOn_limit

added theorem SuccOrder.prelimitRecOn_of_isSuccPrelimit

deleted theorem SuccOrder.prelimitRecOn_succ'

added theorem SuccOrder.prelimitRecOn_succ_of_not_isMax

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean