mathlib

mathlib copied to clipboard

• Add new files dfinsupp/ne_locus and dfinsupp/lex mostly by copying the finsupp counterparts and making trivial adaptions. Use the dfinsupp lemmas/constructions to golf the finsupp counterpart, e.g. the linear_order on finsupp.lex.

• Add lemmas lex_lt_of_lt(_of_preorder) for each of pi/finsupp/dfinsupp that shows the (<) relation on the product of a family of partial orders is a subrelation of the lexicographic (<), for any choice of well-founded relation (in the case of pi) or strict total order (in the case of (d)finsupp) on the set of coordinates. Useful to deduce well-foundedness of the product order from the well-foundedness of the lexicographic order in #16772.

---

Just a heads-up that Anne delegated to me #16236 and I will merge is as soon as CI is happy with it. I'm mentioning this since the PR touches the finsupp.lex file, though only to edit a doc-string, I think.

Oh nevermind we can't multiplicativize because we don't have finitely multiplicatively supported functions. I will open a PR matching the finsupp.ne_locus and dist APIs shortly.

Here's the PR #17036. I don't care whether the current is merged first.

Thanks :tada:

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests