mathlib3

680e8eda - feat(order/well_founded_set): defining `is_partially_well_ordered` to prove `is_wf.add` (#6226)

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`