Lemmas about the
inf of the support of
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
The current plan is to state and prove lemmas about
finset.sup (finsupp.support f) D with a
"generic" degree/weight function
D from the grading Type
A to a somewhat ordered Type
Next, the general lemmas get specialized for some yet-to-be-defined
In this section, we use
degt to denote "degree functions" on
A with values in
a type with bot or top respectively.