# 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 (x1 x2 : α) => x1 < x2]
[Finite σ]
(S : Set (σ →₀ α))
:

S.IsPWO

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`

.