Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-08 15:56 56e52487

View on Github →

feat(order/order_iso_nat): add another flavour of well-foundedness for partial orders (#5434)

Estimated changes

Modified src/order/order_iso_nat.lean

added theorem well_founded.monotone_chain_condition

Modified src/order/preorder_hom.lean

added theorem rel_embedding.to_preorder_hom_injective

added def rel_hom.to_preorder_hom

added theorem rel_hom.to_preorder_hom_coe_fn