English
Let i ∈ Fin n with i < m and work in the Lex-weighted setting. The lexicographic supremum of esymm with argument (i+1) is equal, via ofLex, to the accumulated degree corresponding to a single 1 at position i, namely accumulate n m (Finsupp.single i 1).
Русский
Пусть i ∈ Fin n и i < m. В подсистеме с весами Lex верхняя грань (supDegree) для esymm с аргументом (i+1) равна accumulate n m (Finsupp.single i 1).
LaTeX
$$$\operatorname{ofLex} (\operatorname{supDegree} \text{toLex} <| \operatorname{esymm} (\operatorname{Fin} m) R (i + 1)) = \operatorname{accumulate} n m (\operatorname{Finsupp.single} i 1)$$$
Lean4
theorem supDegree_esymm [Nontrivial R] (him : i < m) :
ofLex (supDegree toLex <| esymm (Fin m) R (i + 1)) = accumulate n m (Finsupp.single i 1) :=
by
rw [(supDegree_monic_esymm him).1, ofLex_toLex]
ext j
simp_rw [Finsupp.indicator_apply, dite_eq_ite, mem_Iic, accumulate_apply, Finsupp.single_apply, sum_ite_eq,
mem_filter_univ, Fin.le_def]
