mathlib3

923314f2 - refactor(order/well_founded_set): partially well ordered sets using relations other than `has_le.le` (#7131)

refactor(order/well_founded_set): partially well ordered sets using relations other than `has_le.le` (#7131) Introduces `set.partially_well_ordered_on` to generalize `set.is_partially_well_ordered` to relations that do not necessarily come from a `has_le` instance Renames `set.is_partially_well_ordered` to `set.is_pwo` in analogy with `set.is_wf` Prepares to refactor Hahn series to use `set.is_pwo` and avoid the assumption of a linear order