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
instance
Finsupp.wellQuasiOrderedLE
{α : Type u_1}
{σ : Type u_2}
[Zero α]
[Preorder α]
[WellQuasiOrderedLE α]
[Finite σ]
:
WellQuasiOrderedLE (σ →₀ α)
A version of Dickson's lemma: σ →₀ α is well-quasi-ordered when σ is Finite and α is
well-quasi-ordered.
This version uses finsupps on a finite type as it is intended for use with MVPowerSeries.