Mathlib Changelog
v4
Changelog
About
Github
Theorem
WellFoundedGT.iSup_eq_monotonicSequenceLimit
Modification history
2025-02-08 23:59
Mathlib/Order/OrderIsoNat.lean
refactor(Order/OrderIsoNat): use `WellFoundedGT` in monotone chain condition (#20782) …
Added
WellFoundedGT.iSup_eq_monotonicSequenceLimit
View on Github →