Commit 2024-10-02 17:17 c669fd15

View on Github →

refactor(Data/Real/Archimedean): sSup/sInf API cleanup (#16735) Add a few lemmas, golf the existing ones and update the docstrings to something more precise

Estimated changes

modified theorem Real.add_neg_lt_sSup
deleted theorem Real.ciInf_const_zero
deleted theorem Real.ciSup_const_zero
modified theorem Real.exists_isGLB
modified theorem Real.exists_isLUB
added theorem Real.iInf_const_zero
modified theorem Real.iInf_nonneg
added theorem Real.iInf_nonpos'
added theorem Real.iInf_nonpos
modified theorem Real.iInf_of_not_bddBelow
added theorem Real.iSup_const_zero
added theorem Real.iSup_nonneg'
added theorem Real.iSup_nonneg
added theorem Real.iSup_nonpos
modified theorem Real.iSup_of_isEmpty
modified theorem Real.iSup_of_not_bddAbove
modified theorem Real.le_sSup_iff
modified theorem Real.lt_sInf_add_pos
modified theorem Real.sInf_def
modified theorem Real.sInf_le_iff
modified theorem Real.sInf_nonneg
added theorem Real.sInf_nonpos'
modified theorem Real.sInf_nonpos
modified theorem Real.sInf_of_not_bddBelow
modified theorem Real.sSup_def
added theorem Real.sSup_nonneg'
modified theorem Real.sSup_nonneg
modified theorem Real.sSup_nonpos
modified theorem Real.sSup_of_not_bddAbove