Documentation

Mathlib.Data.Finsupp.PWO

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 (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.