Mathlib Changelog
v4
Changelog
About
Github
Theorem
Set.range_injOn_strictMono_of_wellFoundedLT
Modification history
2026-08-24 11:53
Mathlib/Order/WellFounded.lean
chore(Order/WellFounded): use `to_dual` (#39438) …
Added
Set.range_injOn_strictMono_of_wellFoundedLT
View on Github →