Commit 2021-10-14 23:10 c37ea535

View on Github →

feat(order/succ_pred): succ-Archimedean orders (#9714) This defines succ-Archimedean orders: orders in which a ≤ b means that succ^[n] a = b for some n.

Estimated changes

Modified src/logic/function/iterate.lean

added def function.iterate.rec

added theorem function.iterate.rec_zero

Modified src/order/succ_pred.lean

added theorem exists_pred_iterate_iff_le

added theorem exists_pred_iterate_or

added theorem exists_succ_iterate_iff_le

added theorem exists_succ_iterate_or

added theorem has_le.le.exists_pred_iterate

added theorem has_le.le.exists_succ_iterate

added theorem pred.rec

added theorem pred.rec_iff

added theorem pred.rec_linear

added theorem pred.rec_top

added theorem succ.rec

added theorem succ.rec_bot

added theorem succ.rec_iff

added theorem succ.rec_linear