Finsupp.isPWO

theorem Finsupp.isPWO : ∀ {α : Type u_1} {σ : Type u_2} [inst : Zero α] [inst_1 : LinearOrder α] [inst_2 : IsWellOrder α fun x x_1 => x < x_1] [inst_3 : Finite σ] (S : Set (σ →₀ α)), S.IsPWO

This theorem is a version of **Dickson's lemma** that asserts that any subset of functions from `σ` to `α` is partially well-ordered, under the condition that `σ` is finite and `α` is a linear well order. Here, the functions are represented as finsupps, a specific type of function in Lean that maps most inputs to zero and is intended for use with multivariate power series (denoted as `MVPowerSeries` in the code). A partially well-ordered set is a set where every non-empty subset has a least element under some ordering.

More concisely: Given a finite set σ and a linear well-ordered set α, every non-empty subset of functions from σ to α has a least element under the pointwise ordering of finsupps.