Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-09 14:41 4fc47d5f

View on Github →

feat(set_theory/*): Miscellaneous lemmas (#16854) A few simple lemmas about cardinals and ordinals.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.subsingleton.coe_sort

Modified src/set_theory/cardinal/basic.lean

added theorem cardinal.le_mk_diff_add_mk

added theorem cardinal.mk_diff_add_mk

added theorem cardinal.mk_le_one_iff_set_subsingleton

Modified src/set_theory/ordinal/basic.lean

added theorem Well_order.eta

added theorem ordinal.type_out