Commit 2024-05-21 16:45 27b3df77

feat: SuccOrder and recursion principle on well-ordered type (#11290) Order/SuccPred/Basic.lean: add SuccOrder.ofLinearWellFoundedLT, which puts a SuccOrder on an arbitrary well-ordered type. Also add the dual, PredOrder version. Add missing pred lemmas corresponding to existing succ lemmas. Order/SuccPred/Limit.lean: add SuccOrder.limitRecOn generalizing Ordinal.limitRecOn to allow definition by transfinite recursion on an arbitrary well-ordered type. (It turns out a partial well-founded order is enough.) SetTheory/Ordinal/Arithmetic.lean: refactor Ordinal.limitRecOn to use SuccOrder.limitRecOn. SetTheory/Cardinal/Ordinal.lean: add a lemma saying that the initial ordinal of an infinite cardinal is a NoMaxOrder. SetTheory/Ordinal/Basic.lean: add mk_Iio_ord_out_α, a restatement of card_typein_out_lt.