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 #

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.