Commit 2025-03-18 10:08 621dd319

View on Github →

chore(SetTheory): split Ordinal/Arithmetic.lean (#23017) This splits SetTheory.Ordinal.Arithmetic into two parts by taking out all the material on indexed families of ordinals (sup, bsub, ...) and moving it into Ordinal.Families. Ordinal.Arithmetic contains the initial segment of the original file, plus some lemmas that could be upstreamed. One change: add_le_of_limit is no longer private, since it is used in Arithmetic.lean and Families.lean.

Estimated changes

deleted theorem Ordinal.IsNormal.blsub_eq
deleted theorem Ordinal.IsNormal.bsup
deleted theorem Ordinal.IsNormal.bsup_eq
deleted theorem Ordinal.IsNormal.map_iSup
deleted theorem Ordinal.IsNormal.map_sSup
deleted theorem Ordinal.IsNormal.sup
deleted theorem Ordinal.bddAbove_image
deleted theorem Ordinal.bddAbove_of_small
deleted theorem Ordinal.bddAbove_range
deleted def Ordinal.blsub
deleted theorem Ordinal.blsub_comp
deleted theorem Ordinal.blsub_congr
deleted theorem Ordinal.blsub_const
deleted theorem Ordinal.blsub_eq_blsub
deleted theorem Ordinal.blsub_eq_lsub'
deleted theorem Ordinal.blsub_eq_lsub
deleted theorem Ordinal.blsub_eq_zero_iff
deleted theorem Ordinal.blsub_id
deleted theorem Ordinal.blsub_le
deleted theorem Ordinal.blsub_le_iff
deleted theorem Ordinal.blsub_one
deleted theorem Ordinal.blsub_pos
deleted theorem Ordinal.blsub_type
deleted theorem Ordinal.blsub_zero
deleted def Ordinal.blsub₂
deleted def Ordinal.bmex
deleted theorem Ordinal.bmex_le_blsub
deleted theorem Ordinal.bmex_le_of_ne
deleted theorem Ordinal.bmex_monotone
deleted def Ordinal.brange
deleted theorem Ordinal.brange_const
deleted def Ordinal.bsup
deleted theorem Ordinal.bsup_comp
deleted theorem Ordinal.bsup_congr
deleted theorem Ordinal.bsup_const
deleted theorem Ordinal.bsup_eq_blsub
deleted theorem Ordinal.bsup_eq_bsup
deleted theorem Ordinal.bsup_eq_sup'
deleted theorem Ordinal.bsup_eq_sup
deleted theorem Ordinal.bsup_eq_zero_iff
deleted theorem Ordinal.bsup_id_limit
deleted theorem Ordinal.bsup_id_succ
deleted theorem Ordinal.bsup_le
deleted theorem Ordinal.bsup_le_blsub
deleted theorem Ordinal.bsup_le_iff
deleted theorem Ordinal.bsup_one
deleted theorem Ordinal.bsup_succ_of_mono
deleted theorem Ordinal.bsup_zero
deleted theorem Ordinal.exists_of_lt_bmex
deleted theorem Ordinal.exists_of_lt_mex
deleted theorem Ordinal.iSup_add_nat
deleted theorem Ordinal.iSup_eq_bsup
deleted theorem Ordinal.iSup_eq_zero_iff
deleted theorem Ordinal.iSup_mul_nat
deleted theorem Ordinal.iSup_natCast
deleted theorem Ordinal.iSup_ord
deleted theorem Ordinal.iSup_succ
deleted theorem Ordinal.iSup_sum
deleted theorem Ordinal.le_bmex_of_forall
deleted theorem Ordinal.le_bsup
deleted theorem Ordinal.le_mex_of_forall
deleted theorem Ordinal.le_sup
deleted def Ordinal.lsub
deleted theorem Ordinal.lsub_const
deleted theorem Ordinal.lsub_empty
deleted theorem Ordinal.lsub_eq_blsub'
deleted theorem Ordinal.lsub_eq_blsub
deleted theorem Ordinal.lsub_eq_lsub
deleted theorem Ordinal.lsub_eq_zero_iff
deleted theorem Ordinal.lsub_le
deleted theorem Ordinal.lsub_le_iff
deleted theorem Ordinal.lsub_le_sup_succ
deleted theorem Ordinal.lsub_pos
deleted theorem Ordinal.lsub_sum
deleted theorem Ordinal.lsub_typein
deleted theorem Ordinal.lsub_unique
deleted theorem Ordinal.lt_add_of_limit
deleted theorem Ordinal.lt_blsub
deleted theorem Ordinal.lt_blsub_iff
deleted theorem Ordinal.lt_blsub₂
deleted theorem Ordinal.lt_bsup
deleted theorem Ordinal.lt_bsup_of_limit
deleted theorem Ordinal.lt_lsub
deleted theorem Ordinal.lt_lsub_iff
deleted theorem Ordinal.mem_brange
deleted theorem Ordinal.mem_brange_self
deleted def Ordinal.mex
deleted theorem Ordinal.mex_le_lsub
deleted theorem Ordinal.mex_le_of_ne
deleted theorem Ordinal.mex_monotone
deleted theorem Ordinal.mex_not_mem_range
deleted theorem Ordinal.ne_bmex
deleted theorem Ordinal.ne_mex
deleted theorem Ordinal.ne_sup_iff_lt_sup
deleted theorem Ordinal.sSup_eq_bsup
deleted theorem Ordinal.sSup_ord
deleted def Ordinal.sup
deleted theorem Ordinal.sup_const
deleted theorem Ordinal.sup_eq_bsup'
deleted theorem Ordinal.sup_eq_bsup
deleted theorem Ordinal.sup_eq_lsub
deleted theorem Ordinal.sup_eq_sup
deleted theorem Ordinal.sup_le
deleted theorem Ordinal.sup_le_iff
deleted theorem Ordinal.sup_le_lsub
deleted theorem Ordinal.sup_succ_eq_lsub
deleted theorem Ordinal.sup_succ_le_lsub
deleted theorem Ordinal.sup_sum
deleted theorem Ordinal.sup_typein_limit
deleted theorem Ordinal.sup_typein_succ
deleted theorem Ordinal.sup_unique
deleted theorem not_injective_of_ordinal
deleted theorem not_small_ordinal
deleted theorem not_surjective_of_ordinal
added theorem Ordinal.IsNormal.bsup
added theorem Ordinal.IsNormal.sup
added theorem Ordinal.bddAbove_image
added theorem Ordinal.bddAbove_range
added def Ordinal.blsub
added theorem Ordinal.blsub_comp
added theorem Ordinal.blsub_congr
added theorem Ordinal.blsub_const
added theorem Ordinal.blsub_eq_blsub
added theorem Ordinal.blsub_eq_lsub'
added theorem Ordinal.blsub_eq_lsub
added theorem Ordinal.blsub_id
added theorem Ordinal.blsub_le
added theorem Ordinal.blsub_le_iff
added theorem Ordinal.blsub_one
added theorem Ordinal.blsub_pos
added theorem Ordinal.blsub_type
added theorem Ordinal.blsub_zero
added def Ordinal.blsub₂
added def Ordinal.bmex
added theorem Ordinal.bmex_le_blsub
added theorem Ordinal.bmex_le_of_ne
added theorem Ordinal.bmex_monotone
added def Ordinal.brange
added theorem Ordinal.brange_const
added def Ordinal.bsup
added theorem Ordinal.bsup_comp
added theorem Ordinal.bsup_congr
added theorem Ordinal.bsup_const
added theorem Ordinal.bsup_eq_blsub
added theorem Ordinal.bsup_eq_bsup
added theorem Ordinal.bsup_eq_sup'
added theorem Ordinal.bsup_eq_sup
added theorem Ordinal.bsup_id_limit
added theorem Ordinal.bsup_id_succ
added theorem Ordinal.bsup_le
added theorem Ordinal.bsup_le_blsub
added theorem Ordinal.bsup_le_iff
added theorem Ordinal.bsup_one
added theorem Ordinal.bsup_zero
added theorem Ordinal.iSup_add_nat
added theorem Ordinal.iSup_eq_bsup
added theorem Ordinal.iSup_mul_nat
added theorem Ordinal.iSup_natCast
added theorem Ordinal.iSup_ord
added theorem Ordinal.iSup_succ
added theorem Ordinal.iSup_sum
added theorem Ordinal.le_bsup
added theorem Ordinal.le_sup
added def Ordinal.lsub
added theorem Ordinal.lsub_const
added theorem Ordinal.lsub_empty
added theorem Ordinal.lsub_eq_blsub'
added theorem Ordinal.lsub_eq_blsub
added theorem Ordinal.lsub_eq_lsub
added theorem Ordinal.lsub_le
added theorem Ordinal.lsub_le_iff
added theorem Ordinal.lsub_pos
added theorem Ordinal.lsub_sum
added theorem Ordinal.lsub_typein
added theorem Ordinal.lsub_unique
added theorem Ordinal.lt_blsub
added theorem Ordinal.lt_blsub_iff
added theorem Ordinal.lt_blsub₂
added theorem Ordinal.lt_bsup
added theorem Ordinal.lt_lsub
added theorem Ordinal.lt_lsub_iff
added theorem Ordinal.mem_brange
added def Ordinal.mex
added theorem Ordinal.mex_le_lsub
added theorem Ordinal.mex_le_of_ne
added theorem Ordinal.mex_monotone
added theorem Ordinal.ne_bmex
added theorem Ordinal.ne_mex
added theorem Ordinal.sSup_eq_bsup
added theorem Ordinal.sSup_ord
added def Ordinal.sup
added theorem Ordinal.sup_const
added theorem Ordinal.sup_eq_bsup'
added theorem Ordinal.sup_eq_bsup
added theorem Ordinal.sup_eq_lsub
added theorem Ordinal.sup_eq_sup
added theorem Ordinal.sup_le
added theorem Ordinal.sup_le_iff
added theorem Ordinal.sup_le_lsub
added theorem Ordinal.sup_sum
added theorem Ordinal.sup_unique
added theorem not_small_ordinal