Theorem IsChain.finite_of_wellFoundedLT_of_wellFoundedGT

Modification history

2026-09-05 15:48
Mathlib/Order/OrderIsoNat.lean
feat(Order/OrderIsoNat): every chain is finite when `<` and `>` are well-founded (#42633) …
Added IsChain.finite_of_wellFoundedLT_of_wellFoundedGTView on Github →