# Partial well ordering on finsupps #

This file contains the fact that finitely supported functions from a fintype are
partially well ordered when the codomain is a linear order that is well ordered.
It is in a separate file for now so as to not add imports to the file `Order.WellFoundedSet`

.

## Main statements #

`Finsupp.isPwo`

- finitely supported functions from a fintype are partially well ordered when the codomain is a linear order that is well ordered

## Tags #

Dickson, order, partial well order

theorem
Finsupp.isPwo
{α : Type u_1}
{σ : Type u_2}
[Zero α]
[LinearOrder α]
[IsWellOrder α fun x x_1 => x < x_1]
[Finite σ]
(S : Set (σ →₀ α))
:

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`

.