mathlib

7b4a9e5f - feat(order/well_founded_set) : Define when a set is well-founded with `set.is_wf` (#6113)

feat(order/well_founded_set) : Define when a set is well-founded with `set.is_wf` (#6113) Defines a predicate for when a set within an ordered type is well-founded (`set.is_wf`) Proves basic lemmas about well-founded sets