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.