Commit 2023-02-12 23:44 7c6b7624

View on Github →

feat: port Data.Dfinsupp.Lex (#2199)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Dfinsupp/Lex.lean

added theorem Dfinsupp.lex_def

added theorem Dfinsupp.lex_lt_of_lt

added theorem Dfinsupp.lex_lt_of_lt_of_preorder

added theorem Dfinsupp.lt_of_forall_lt_of_lt

added theorem Dfinsupp.toLex_monotone

added theorem Pi.lex_eq_dfinsupp_lex