Commit 2023-01-24 13:10 805f2c31

View on Github →

feat: port Order.OrderIsoNat (#1753)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/OrderIsoNat.lean

added theorem Nat.Subtype.orderIsoOfNat_apply

added theorem Nat.coe_orderEmbeddingOfSet

added theorem Nat.exists_subseq_of_forall_mem_union

added def Nat.orderEmbeddingOfSet

added theorem Nat.orderEmbeddingOfSet_apply

added theorem Nat.orderEmbeddingOfSet_range

added theorem RelEmbedding.acc_iff_no_decreasing_seq

added theorem RelEmbedding.coe_natGt

added theorem RelEmbedding.coe_natLt

added theorem RelEmbedding.exists_not_acc_lt_of_not_acc

added def RelEmbedding.natGt

added def RelEmbedding.natLt

added theorem RelEmbedding.not_acc_of_decreasing_seq

added theorem RelEmbedding.not_wellFounded_of_decreasing_seq

added theorem RelEmbedding.wellFounded_iff_no_descending_seq

added theorem WellFounded.monotone_chain_condition'

added theorem WellFounded.monotone_chain_condition

added theorem WellFounded.supᵢ_eq_monotonicSequenceLimit

added theorem exists_increasing_or_nonincreasing_subseq'

added theorem exists_increasing_or_nonincreasing_subseq