Commit 2022-08-25 00:16 4b440bb0

refactor(order/well_founded_set): golf, review API (#11303)

New lemmas

About set.well_founded_on

• set.well_founded_on.mono, set.well_founded_on.mono_set;
• set.well_founded_on.union, set.well_founded_on_union, finset.well_founded_on, set.finite.well_founded_on, set.subsingleton.well_founded_on, set.well_founded_on_empty, set.well_founded_on_singleton, set.well_founded_on_insert, set.well_founded_on.insert;

About set.is_wf

• set.is_wf_union;
• set.finite.is_wf, finset.is_wf, set.is_wf_empty, set.is_wf_singleton, set.subsingleton.is_wf, set.is_wf_insert, set.is_wf.insert;
• finset.is_wf_bUnion

About set.partially_well_ordered_on

• set.partially_well_ordered_on.union, set.partially_well_ordered_on_union;
• set.finite.partially_well_ordered_on, finset.partially_well_ordered_on, set.partially_well_ordered_on_empty, set.partially_well_ordered_on_singleton, set.partially_well_ordered_on_insert (an iff), set.partially_well_ordered_on.insert, set.subsingleton.partially_well_ordered_on;

About set.is_pwo

• set.is_pwo.image_of_monotone_on, set.is_pwo_union;
• finset.is_pwo, set.is_pwo_insert;
• finset.is_pwo_bUnion;

Other API changes

• Definitions lemmas now use ∀ n, f n ∈ s instead of range f ⊆ s.
• Many lemmas now use weaker TC assumptions (e.g., preorder instead of partial_order).
• set.is_wf_iff_no_descending_seq now uses (f : ℕ → α) (hf : strict_anti f) instead of f : order_dual ℕ ↪o α.
• The order of binders in the hf argument of set.partially_well_ordered_on.image_of_monotone_on was changed to match monotone_on.
• set.is_pwo.prod now allows sets from different types.
• finset.is_wf_sup and finset.is_pwo_sup are now iffs