Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-12 14:37 fef5124e

View on Github →

feat(order/order_iso_nat): generalize well_founded.monotone_chain_condition to preorders (#15073) We also clean up the spacing throughout the file.

Estimated changes

Modified src/order/order_iso_nat.lean

modified theorem exists_increasing_or_nonincreasing_subseq'

modified theorem exists_increasing_or_nonincreasing_subseq

modified theorem nat.exists_subseq_of_forall_mem_union

modified theorem nat.subtype.order_iso_of_nat_apply

modified def rel_embedding.nat_gt

modified theorem rel_embedding.nat_lt_apply

added theorem well_founded.monotone_chain_condition'

modified theorem well_founded.monotone_chain_condition

modified theorem well_founded.supr_eq_monotonic_sequence_limit

Modified src/order/well_founded_set.lean

Modified src/ring_theory/artinian.lean