Commit 2023-12-19 09:58 fdcf8b66

View on Github →

feat: Relation between IsSuccLimit and iSup. (#8842)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SuccPred/CompleteLinearOrder.lean

added theorem IsGLB.exists_of_nonempty_of_not_isPredLimit

added theorem IsGLB.exists_of_not_isPredLimit

added theorem IsGLB.mem_of_nonempty_of_not_isPredLimit

added theorem IsGLB.mem_of_not_isPredLimit

added theorem IsLUB.exists_of_nonempty_of_not_isSuccLimit

added theorem IsLUB.exists_of_not_isSuccLimit

added theorem IsLUB.mem_of_nonempty_of_not_isSuccLimit

added theorem IsLUB.mem_of_not_isSuccLimit

added theorem csInf_mem_of_not_isPredLimit

added theorem csSup_mem_of_not_isSuccLimit'

added theorem csSup_mem_of_not_isSuccLimit

added theorem exists_eq_ciInf_of_not_isPredLimit

added theorem exists_eq_ciSup_of_not_isSuccLimit'

added theorem exists_eq_ciSup_of_not_isSuccLimit

added theorem exists_eq_iInf_of_not_isPredLimit

added theorem exists_eq_iSup_of_not_isSuccLimit

added theorem sInf_mem_of_not_isPredLimit

added theorem sSup_mem_of_not_isSuccLimit

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.exists_eq_natCast_of_iSup_eq

added theorem Cardinal.exists_eq_of_iSup_eq_of_not_isLimit

added theorem Cardinal.exists_eq_of_iSup_eq_of_not_isSuccLimit

added theorem Cardinal.not_isLimit_natCast