Theorem Finite.of_wellFoundedLT_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) …
Deleted Finite.of_wellFoundedLT_wellFoundedGTView on Github →
2026-07-13 17:10
Mathlib/Order/OrderIsoNat.lean
feat(Order/OrderIsoNat+Data/Finset/Sort): add finiteness and identity theorems for linear orders (#41679) …
Added Finite.of_wellFoundedLT_wellFoundedGTView on Github →