Commit 2022-03-28 09:53 c030dd2a

View on Github →

feat(set_theory/cardinal): cardinal.to_nat is order-preserving on finite cardinals (#12763) This PR proves that cardinal.to_nat is order-preserving on finite cardinals.

Estimated changes

Modified src/set_theory/cardinal.lean

added theorem cardinal.to_nat_le_iff_le_of_lt_omega

added theorem cardinal.to_nat_le_of_le_of_lt_omega

added theorem cardinal.to_nat_lt_iff_lt_of_lt_omega

added theorem cardinal.to_nat_lt_of_lt_of_lt_omega