mathlib documentation


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 #

Tags #

Dickson, order, partial well order

theorem finsupp.is_pwo {α : Type u_1} {σ : Type u_2} [has_zero α] [linear_order α] [is_well_order α] [fintype σ] (S : set →₀ α)) :

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.