Commit 2024-09-06 21:42 77577996

View on Github →

refactor(Order/SuccPred/Limit): IsSuccLimit → IsSuccPrelimit (#16518) A future PR will redefine IsSuccLimit as a non-minimal IsSuccPrelimit. This matches standard usage for ordinals and cardinals. The "pre-" in the name was chosen by analogy to e.g. PreconnectedSpace. Every theorem that previously used isSuccLimit in its name is deprecated. Some of these will be overwritten once IsSuccLimit is defined.

Estimated changes

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

deleted theorem IsGLB.exists_of_nonempty_of_not_isPredLimit

added theorem IsGLB.exists_of_nonempty_of_not_isPredPrelimit

deleted theorem IsGLB.exists_of_not_isPredLimit

added theorem IsGLB.exists_of_not_isPredPrelimit

deleted theorem IsGLB.mem_of_nonempty_of_not_isPredLimit

added theorem IsGLB.mem_of_nonempty_of_not_isPredPrelimit

deleted theorem IsGLB.mem_of_not_isPredLimit

added theorem IsGLB.mem_of_not_isPredPrelimit

deleted theorem IsLUB.exists_of_nonempty_of_not_isSuccLimit

added theorem IsLUB.exists_of_nonempty_of_not_isSuccPrelimit

deleted theorem IsLUB.exists_of_not_isSuccLimit

added theorem IsLUB.exists_of_not_isSuccPrelimit

deleted theorem IsLUB.mem_of_nonempty_of_not_isSuccLimit

added theorem IsLUB.mem_of_nonempty_of_not_isSuccPrelimit

deleted theorem IsLUB.mem_of_not_isSuccLimit

added theorem IsLUB.mem_of_not_isSuccPrelimit

deleted theorem csInf_mem_of_not_isPredLimit

added theorem csInf_mem_of_not_isPredPrelimit

deleted theorem csSup_mem_of_not_isSuccLimit'

deleted theorem csSup_mem_of_not_isSuccLimit

added theorem csSup_mem_of_not_isSuccPrelimit'

added theorem csSup_mem_of_not_isSuccPrelimit

deleted theorem exists_eq_ciInf_of_not_isPredLimit

added theorem exists_eq_ciInf_of_not_isPredPrelimit

deleted theorem exists_eq_ciSup_of_not_isSuccLimit'

deleted theorem exists_eq_ciSup_of_not_isSuccLimit

added theorem exists_eq_ciSup_of_not_isSuccPrelimit'

added theorem exists_eq_ciSup_of_not_isSuccPrelimit

deleted theorem exists_eq_iInf_of_not_isPredLimit

added theorem exists_eq_iInf_of_not_isPredPrelimit

deleted theorem exists_eq_iSup_of_not_isSuccLimit

added theorem exists_eq_iSup_of_not_isSuccPrelimit

deleted theorem sInf_mem_of_not_isPredLimit

added theorem sInf_mem_of_not_isPredPrelimit

deleted theorem sSup_mem_of_not_isSuccLimit

added theorem sSup_mem_of_not_isSuccPrelimit

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem Order.IsPredLimit.lt_pred

deleted theorem Order.IsPredLimit.lt_pred_iff

deleted theorem Order.IsPredLimit.pred_ne

deleted def Order.IsPredLimit

added theorem Order.IsPredPrelimit.lt_pred

added theorem Order.IsPredPrelimit.lt_pred_iff

added theorem Order.IsPredPrelimit.pred_ne

added def Order.IsPredPrelimit

deleted theorem Order.IsSuccLimit.isMin_of_noMax

deleted theorem Order.IsSuccLimit.succ_lt

deleted theorem Order.IsSuccLimit.succ_lt_iff

deleted theorem Order.IsSuccLimit.succ_ne

deleted def Order.IsSuccLimit

added theorem Order.IsSuccPrelimit.isMin_of_noMax

added theorem Order.IsSuccPrelimit.succ_lt

added theorem Order.IsSuccPrelimit.succ_lt_iff

added theorem Order.IsSuccPrelimit.succ_ne

added def Order.IsSuccPrelimit

deleted theorem Order.isPredLimitRecOn_limit

deleted theorem Order.isPredLimitRecOn_pred'

deleted theorem Order.isPredLimitRecOn_pred

deleted theorem Order.isPredLimit_iff

deleted theorem Order.isPredLimit_iff_lt_pred

deleted theorem Order.isPredLimit_iff_of_noMin

deleted theorem Order.isPredLimit_of_dense

deleted theorem Order.isPredLimit_of_pred_lt

deleted theorem Order.isPredLimit_of_pred_ne

deleted theorem Order.isPredLimit_toDual_iff

deleted theorem Order.isPredLimit_top

added theorem Order.isPredPrelimitRecOn_limit

added theorem Order.isPredPrelimitRecOn_pred'

added theorem Order.isPredPrelimitRecOn_pred

added theorem Order.isPredPrelimit_iff

added theorem Order.isPredPrelimit_iff_lt_pred

added theorem Order.isPredPrelimit_iff_of_noMin

added theorem Order.isPredPrelimit_of_dense

added theorem Order.isPredPrelimit_of_pred_lt

added theorem Order.isPredPrelimit_of_pred_ne

added theorem Order.isPredPrelimit_toDual_iff

added theorem Order.isPredPrelimit_top

deleted theorem Order.isSuccLimitRecOn_limit

deleted theorem Order.isSuccLimitRecOn_succ'

deleted theorem Order.isSuccLimitRecOn_succ

deleted theorem Order.isSuccLimit_bot

deleted theorem Order.isSuccLimit_iff

deleted theorem Order.isSuccLimit_iff_of_noMax

deleted theorem Order.isSuccLimit_iff_succ_lt

deleted theorem Order.isSuccLimit_iff_succ_ne

deleted theorem Order.isSuccLimit_of_dense

deleted theorem Order.isSuccLimit_of_succ_lt

deleted theorem Order.isSuccLimit_of_succ_ne

deleted theorem Order.isSuccLimit_toDual_iff

added theorem Order.isSuccPrelimitRecOn_limit

added theorem Order.isSuccPrelimitRecOn_succ'

added theorem Order.isSuccPrelimitRecOn_succ

added theorem Order.isSuccPrelimit_bot

added theorem Order.isSuccPrelimit_iff

added theorem Order.isSuccPrelimit_iff_of_noMax

added theorem Order.isSuccPrelimit_iff_succ_lt

added theorem Order.isSuccPrelimit_iff_succ_ne

added theorem Order.isSuccPrelimit_of_dense

added theorem Order.isSuccPrelimit_of_succ_lt

added theorem Order.isSuccPrelimit_of_succ_ne

added theorem Order.isSuccPrelimit_toDual_iff

deleted theorem Order.mem_range_pred_of_not_isPredLimit

added theorem Order.mem_range_pred_of_not_isPredPrelimit

deleted theorem Order.mem_range_pred_or_isPredLimit

added theorem Order.mem_range_pred_or_isPredPrelimit

deleted theorem Order.mem_range_succ_of_not_isSuccLimit

added theorem Order.mem_range_succ_of_not_isSuccPrelimit

deleted theorem Order.mem_range_succ_or_isSuccLimit

added theorem Order.mem_range_succ_or_isSuccPrelimit

deleted theorem Order.not_isPredLimit

deleted theorem Order.not_isPredLimit_iff

deleted theorem Order.not_isPredLimit_iff_exists_covBy

deleted theorem Order.not_isPredLimit_of_noMin

deleted theorem Order.not_isPredLimit_pred

deleted theorem Order.not_isPredLimit_pred_of_not_isMin

added theorem Order.not_isPredPrelimit

added theorem Order.not_isPredPrelimit_iff

added theorem Order.not_isPredPrelimit_iff_exists_covBy

added theorem Order.not_isPredPrelimit_of_noMin

added theorem Order.not_isPredPrelimit_pred

added theorem Order.not_isPredPrelimit_pred_of_not_isMin

deleted theorem Order.not_isSuccLimit

deleted theorem Order.not_isSuccLimit_iff'

deleted theorem Order.not_isSuccLimit_iff

deleted theorem Order.not_isSuccLimit_iff_exists_covBy

deleted theorem Order.not_isSuccLimit_of_noMax

deleted theorem Order.not_isSuccLimit_succ

deleted theorem Order.not_isSuccLimit_succ_of_not_isMax

added theorem Order.not_isSuccPrelimit

added theorem Order.not_isSuccPrelimit_iff'

added theorem Order.not_isSuccPrelimit_iff

added theorem Order.not_isSuccPrelimit_iff_exists_covBy

added theorem Order.not_isSuccPrelimit_of_noMax

added theorem Order.not_isSuccPrelimit_succ

added theorem Order.not_isSuccPrelimit_succ_of_not_isMax

deleted theorem PredOrder.limitRecOn_limit

deleted theorem PredOrder.limitRecOn_pred

added theorem PredOrder.prelimitRecOn_limit

added theorem PredOrder.prelimitRecOn_pred

deleted theorem SuccOrder.limitRecOn_limit

deleted theorem SuccOrder.limitRecOn_succ

added theorem SuccOrder.prelimitRecOn_limit

added theorem SuccOrder.prelimitRecOn_succ

Modified Mathlib/SetTheory/Cardinal/Basic.lean

deleted theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit

added theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccPrelimit

deleted theorem Cardinal.isSuccLimit_aleph0

deleted theorem Cardinal.isSuccLimit_zero

added theorem Cardinal.isSuccPrelimit_aleph0

added theorem Cardinal.isSuccPrelimit_zero

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Cardinal.isStrongLimit_beth

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.IsLimit.isSuccLimit

added theorem Ordinal.IsLimit.isSuccPrelimit

deleted theorem Ordinal.isSuccLimit_zero

added theorem Ordinal.isSuccPrelimit_zero