Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finsupp.lex.le_of_of_lex_le

Modification history

2022-10-24 07:29
src/data/finsupp/lex.lean
feat(data): port finsupp.ne_locus/lex to dfinsupp (#16777) …
Deleted finsupp.lex.le_of_of_lex_leView on Github →
2022-09-01 11:45
src/data/finsupp/lex.lean
feat(data/finsupp/lex): lexicographic orders on finsupps and covariant classes (#16127) …
Added finsupp.lex.le_of_of_lex_leView on Github →