Commit 2022-11-06 07:48 fe664106

View on Github →

feat(order/order_iso_nat): value is accessible iff it's not contained in an infinite decreasing sequence (#15927) This proves the remark made in the definition of acc.

Estimated changes

Modified src/order/order_iso_nat.lean

added theorem rel_embedding.acc_iff_no_decreasing_seq

added theorem rel_embedding.coe_nat_gt

added theorem rel_embedding.coe_nat_lt

added theorem rel_embedding.exists_not_acc_lt_of_not_acc

modified def rel_embedding.nat_lt

deleted theorem rel_embedding.nat_lt_apply

added theorem rel_embedding.not_acc_of_decreasing_seq

added theorem rel_embedding.not_well_founded_of_decreasing_seq