Commit 2024-10-11 12:40 13c52d66

View on Github →

chore(SetTheory/Cardinal/Ordinal): split file (#16990) We split this file into two:

  • Cardinal/Aleph: contains the definitions for the aleph and beth functions (and soon, the omega function).
  • Cardinal/Arithmetic: any results on cardinal arithmetic that depend on c * c = c (which requires some basic properties of ordinals to be proven) These files are otherwise unchanged, with the exception of tweaking some section headers.

Estimated changes

added def Cardinal.aleph'
added theorem Cardinal.aleph'_le
added theorem Cardinal.aleph'_limit
added theorem Cardinal.aleph'_lt
added theorem Cardinal.aleph'_max
added theorem Cardinal.aleph'_nat
added theorem Cardinal.aleph'_omega0
added theorem Cardinal.aleph'_pos
added theorem Cardinal.aleph'_succ
added theorem Cardinal.aleph'_zero
added def Cardinal.aleph
added theorem Cardinal.alephIdx.init
added theorem Cardinal.alephIdx_le
added theorem Cardinal.alephIdx_lt
added theorem Cardinal.aleph_le
added theorem Cardinal.aleph_le_beth
added theorem Cardinal.aleph_limit
added theorem Cardinal.aleph_lt
added theorem Cardinal.aleph_max
added theorem Cardinal.aleph_pos
added theorem Cardinal.aleph_succ
added theorem Cardinal.aleph_toNat
added theorem Cardinal.aleph_zero
added def Cardinal.beth
added theorem Cardinal.beth_le
added theorem Cardinal.beth_limit
added theorem Cardinal.beth_lt
added theorem Cardinal.beth_mono
added theorem Cardinal.beth_ne_zero
added theorem Cardinal.beth_normal
added theorem Cardinal.beth_pos
added theorem Cardinal.beth_succ
added theorem Cardinal.beth_zero
added theorem Cardinal.exists_aleph
added theorem Cardinal.max_aleph_eq
added theorem Cardinal.mk_cardinal
added theorem Cardinal.succ_aleph0
added theorem Cardinal.type_cardinal
deleted def Cardinal.aleph'
deleted theorem Cardinal.aleph'_alephIdx
deleted theorem Cardinal.aleph'_isNormal
deleted theorem Cardinal.aleph'_le
deleted theorem Cardinal.aleph'_limit
deleted theorem Cardinal.aleph'_lt
deleted theorem Cardinal.aleph'_max
deleted theorem Cardinal.aleph'_nat
deleted theorem Cardinal.aleph'_omega0
deleted theorem Cardinal.aleph'_pos
deleted theorem Cardinal.aleph'_succ
deleted theorem Cardinal.aleph'_zero
deleted theorem Cardinal.aleph0_le_aleph'
deleted theorem Cardinal.aleph0_le_aleph
deleted theorem Cardinal.aleph0_le_beth
deleted def Cardinal.aleph
deleted theorem Cardinal.alephIdx.init
deleted def Cardinal.alephIdx
deleted theorem Cardinal.alephIdx_aleph'
deleted theorem Cardinal.alephIdx_le
deleted theorem Cardinal.alephIdx_lt
deleted theorem Cardinal.aleph_eq_aleph'
deleted theorem Cardinal.aleph_isNormal
deleted theorem Cardinal.aleph_le
deleted theorem Cardinal.aleph_le_beth
deleted theorem Cardinal.aleph_limit
deleted theorem Cardinal.aleph_lt
deleted theorem Cardinal.aleph_max
deleted theorem Cardinal.aleph_pos
deleted theorem Cardinal.aleph_succ
deleted theorem Cardinal.aleph_toNat
deleted theorem Cardinal.aleph_toPartENat
deleted theorem Cardinal.aleph_zero
deleted def Cardinal.beth
deleted theorem Cardinal.beth_le
deleted theorem Cardinal.beth_limit
deleted theorem Cardinal.beth_lt
deleted theorem Cardinal.beth_mono
deleted theorem Cardinal.beth_ne_zero
deleted theorem Cardinal.beth_normal
deleted theorem Cardinal.beth_pos
deleted theorem Cardinal.beth_strictMono
deleted theorem Cardinal.beth_succ
deleted theorem Cardinal.beth_zero
deleted theorem Cardinal.exists_aleph
deleted theorem Cardinal.max_aleph_eq
deleted theorem Cardinal.mk_cardinal
deleted theorem Cardinal.noMaxOrder
deleted theorem Cardinal.ord_isLimit
deleted theorem Cardinal.succ_aleph0
deleted theorem Cardinal.type_cardinal
deleted theorem Ordinal.omega0_lt_omega1
added theorem Cardinal.noMaxOrder
added theorem Cardinal.ord_isLimit