English
If a power series φ is nonzero, there exists a nonempty subset ne of the image of its support under the toLex map such that φ.lexOrder equals the minimal element in that subset under the well-founded order.
Русский
Если ряд φ не равен нулю, существует непустое множество ne образа поддержки φ по отображению toLex, такое что φ.lexOrder совпадает с минимальным элементом этого множества относительно хорошо основанного порядка.
LaTeX
$$$\phi \neq 0 \Rightarrow \exists ne \neq \emptyset,\; \operatorname{lexOrder}(\phi) = \mathrm{WithTop}.\text{some}(\min_{\text{Lex}}(\operatorname{toLex}(\operatorname{support}(\phi))), ne)$$$
Lean4
theorem lexOrder_def_of_ne_zero {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) :
∃ (ne : Set.Nonempty (toLex '' φ.support)),
lexOrder φ =
WithTop.some ((@wellFounded_lt (Lex (σ →₀ ℕ)) (instLTLex) (Lex.wellFoundedLT)).min (toLex '' φ.support) ne) :=
by
suffices ne : Set.Nonempty (toLex '' φ.support) by
use ne
unfold lexOrder
simp only [dif_neg hφ]
simp only [Set.image_nonempty, Function.support_nonempty_iff, ne_eq, hφ, not_false_eq_true]
