Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-21 16:19 99625b1b

View on Github →

feat(set_theory/cardinal/ordinal): basic properties on Beth numbers (#14989) We define Beth cardinals and prove miscellaneous basic properties about them.

Estimated changes

added theorem cardinal.beth_one
added theorem cardinal.aleph'_limit
added theorem cardinal.aleph_le_beth
added theorem cardinal.aleph_limit
added def cardinal.beth
added theorem cardinal.beth_le
added theorem cardinal.beth_limit
added theorem cardinal.beth_lt
added theorem cardinal.beth_ne_zero
added theorem cardinal.beth_pos
added theorem cardinal.beth_succ
added theorem cardinal.beth_zero
added theorem ordinal.le_sub_of_le
deleted theorem ordinal.small_Iio
added theorem ordinal.sub_lt_of_le