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 (σ →₀ α))
:
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.