English
The lexicographic order on multivariate power series is defined by selecting, for a nonzero series, the least exponent in its support with respect to the Lex order on exponent vectors, and assigning top to the zero series.
Русский
Лексикографический порядок на многовариантных рядах задаётся так: для ненулевого ряда выбираем минимальный по лексикографическому порядку вектор степеней из его поддержки; нулевой ряд получает верхнюю позицию.
LaTeX
$$$\operatorname{lexOrder}: \mathrm{MvPowerSeries}(\sigma,R) \to \mathrm{WithTop}(\mathrm{Lex}(\sigma \to\!\mathbb{N}_0))\;\text{ определяется так:}\\$$
Lean4
/-- The lex order on multivariate power series. -/
noncomputable def lexOrder (φ : MvPowerSeries σ R) : (WithTop (Lex (σ →₀ ℕ))) := by
classical
exact
if h : φ = 0 then ⊤
else
by
have ne : Set.Nonempty (toLex '' φ.support) := by
simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, h, not_false_eq_true]
apply WithTop.some
apply WellFounded.min _ (toLex '' φ.support) ne
· exact Finsupp.instLTLex.lt
· exact wellFounded_lt
