English
A version of Dickson's lemma states: any subset S of finsupps σ →₀ α is partially well-ordered when σ is finite and α is a linear well order; this can be realized via an isomorphism with finite-support functions.
Русский
Версия леммы Диксона для finsupp: любая подмножество S функций σ →₀ α частично хорошо упорядочено, если σ конечен и α линейно хорошо упорядочен.
LaTeX
$$$\\text{isPWO}(S)$ for $S \\subseteq (\\sigma \\to_0 α)$ under the pointwise order whenever $σ$ is finite and $α$ is a linear well order$$
Lean4
/-- A version of **Dickson's lemma** any subset of functions `σ →₀ α` is partially well
ordered, when `σ` is `Finite` and `α` is a linear well order.
This version uses finsupps on a finite type as it is intended for use with `MVPowerSeries`.
-/
theorem isPWO {α σ : Type*} [Zero α] [LinearOrder α] [WellFoundedLT α] [Finite σ] (S : Set (σ →₀ α)) : S.IsPWO :=
Finsupp.equivFunOnFinite.symm_image_image S ▸
Set.PartiallyWellOrderedOn.image_of_monotone_on (Pi.isPWO _) fun _a _b _ha _hb => id
