Commit 2024-09-05 05:04 a4692953

View on Github →

chore(Order/SuccPred/Limit): organize induction principles (#16459) We put all of our induction principles at the end of the file, and standardize both argument order and naming. We also golf PredOrder.limitRecOn by defining it in terms of SuccOrder.limitRecOn on the dual order.

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

modified theorem Order.isPredLimitRecOn_limit

modified theorem Order.isPredLimitRecOn_pred'

modified theorem Order.isPredLimitRecOn_pred

modified theorem Order.isSuccLimitRecOn_limit

modified theorem Order.isSuccLimitRecOn_succ'

modified theorem Order.isSuccLimitRecOn_succ

modified theorem PredOrder.limitRecOn_limit

modified theorem PredOrder.limitRecOn_pred

modified theorem SuccOrder.limitRecOn_limit

modified theorem SuccOrder.limitRecOn_succ

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean