Commit 2023-11-13 07:42 43e32656

View on Github →

chore: split Data.Real.Basic (#8356)

Estimated changes

added theorem Real.add_neg_lt_sSup
added theorem Real.cauSeq_converges
added theorem Real.ciInf_const_zero
added theorem Real.ciInf_empty
added theorem Real.ciSup_const_zero
added theorem Real.ciSup_empty
added theorem Real.exists_floor
added theorem Real.exists_isLUB
added theorem Real.iInf_nonneg
added theorem Real.isCauSeq_iff_lift
added theorem Real.le_sSup_iff
added theorem Real.lt_sInf_add_pos
added theorem Real.of_near
added theorem Real.sInf_def
added theorem Real.sInf_empty
added theorem Real.sInf_le_iff
added theorem Real.sInf_le_sSup
added theorem Real.sInf_nonneg
added theorem Real.sInf_nonpos
added theorem Real.sSup_def
added theorem Real.sSup_empty
added theorem Real.sSup_nonneg
added theorem Real.sSup_nonpos
added theorem Real.sSup_univ
deleted theorem Real.add_neg_lt_sSup
deleted theorem Real.cauSeq_converges
deleted theorem Real.ciInf_const_zero
deleted theorem Real.ciInf_empty
deleted theorem Real.ciSup_const_zero
deleted theorem Real.ciSup_empty
deleted theorem Real.exists_floor
deleted theorem Real.exists_isLUB
deleted theorem Real.iInf_nonneg
deleted theorem Real.iInf_of_not_bddBelow
deleted theorem Real.iSup_of_not_bddAbove
deleted theorem Real.isCauSeq_iff_lift
deleted theorem Real.le_sSup_iff
deleted theorem Real.lt_sInf_add_pos
deleted theorem Real.of_near
deleted theorem Real.sInf_def
deleted theorem Real.sInf_empty
deleted theorem Real.sInf_le_iff
deleted theorem Real.sInf_le_sSup
deleted theorem Real.sInf_nonneg
deleted theorem Real.sInf_nonpos
deleted theorem Real.sInf_of_not_bddBelow
deleted theorem Real.sSup_def
deleted theorem Real.sSup_empty
deleted theorem Real.sSup_nonneg
deleted theorem Real.sSup_nonpos
deleted theorem Real.sSup_of_not_bddAbove
deleted theorem Real.sSup_univ