Commit 2021-02-23 06:48 680e8eda

View on Github →

feat(order/well_founded_set): defining is_partially_well_ordered to prove is_wf.add (#6226) Defines set.is_partially_well_ordered s, equivalent to any infinite sequence to s contains an infinite monotone subsequence Provides a basic API for set.is_partially_well_ordered Proves is_wf.add and is_wf.mul

Estimated changes

Modified src/order/well_founded_set.lean

added theorem finset.is_wf_support_mul_antidiagonal

added theorem finset.mul_antidiagonal_mono_left

added theorem finset.mul_antidiagonal_mono_right

added theorem finset.support_mul_antidiagonal_subset_mul

added theorem set.is_partially_well_ordered.exists_monotone_subseq

added theorem set.is_partially_well_ordered.image_of_monotone

added theorem set.is_partially_well_ordered.is_wf

added theorem set.is_partially_well_ordered.mul

added theorem set.is_partially_well_ordered.prod

added def set.is_partially_well_ordered

added theorem set.is_partially_well_ordered_iff_exists_monotone_subseq

modified theorem set.is_wf.insert

added theorem set.is_wf.is_partially_well_ordered

added theorem set.is_wf.mul

added theorem set.is_wf_empty

modified theorem set.is_wf_singleton