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.well_founded_set.
Main statements #
finsupp.is_pwo- 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.is_pwo
{α : Type u_1}
{σ : Type u_2}
[has_zero α]
[linear_order α]
[is_well_order α has_lt.lt]
[fintype σ]
(S : set (σ →₀ α)) :
S.is_pwo
A version of Dickson's lemma any subset of functions σ →₀ α is partially well
ordered, when σ is a fintype and α is a linear well order.
This version uses finsupps on a fintype as it is intended for use with mv_power_series.