Commit 2021-02-11 16:20 7b4a9e5f

View on Github →

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

Estimated changes

Modified src/order/order_iso_nat.lean

added def nat.order_embedding_of_set

added theorem nat.order_embedding_of_set_apply

added theorem nat.order_embedding_of_set_range

added theorem nat.subtype.order_iso_of_nat_apply

modified def rel_embedding.nat_gt

modified def rel_embedding.nat_lt

added theorem rel_embedding.nat_lt_apply

modified theorem rel_embedding.well_founded_iff_no_descending_seq

Modified src/order/rel_iso.lean

added theorem rel_embedding.order_embedding_of_lt_embedding_apply

Created src/order/well_founded_set.lean

added theorem finset.is_wf

added theorem set.finite.is_wf

added theorem set.fintype.is_wf

added theorem set.is_wf.insert

added theorem set.is_wf.mono

added theorem set.is_wf.union

added def set.is_wf

added theorem set.is_wf_iff_no_descending_seq

added theorem set.is_wf_singleton

added def set.well_founded_on

added theorem set.well_founded_on_iff