Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.lt_of_forall_lt_of_lt

Modification history

2022-09-01 11:45
src/data/finsupp/lex.lean
feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127) …
Added finsupp.lt_of_forall_lt_of_ltView on Github →