| Metric | Count |
|---|
| Definitions | 0 |
Theoremsadd_ne_top, Ico_eq_Iio, addLECancellable_iff_ne, addLeftReflectLT, add_biSup, add_biSup', add_eq_top, add_iInf, add_iInf₂, add_iSup, add_le_add_iff_left, add_le_add_iff_right, add_left_inj, add_lt_add, add_lt_add_iff_left, add_lt_add_iff_right, add_lt_add_left, add_lt_add_of_le_of_lt, add_lt_add_of_lt_of_le, add_lt_add_right, add_lt_top, add_ne_top, add_right_inj, add_sInf, add_sSup, add_sub_add_eq_sub_left, add_sub_add_eq_sub_right, add_sub_cancel_left, add_sub_cancel_right, biSup_add, biSup_add', biSup_add_biSup_le, biSup_add_biSup_le', cancel_coe, cancel_of_lt, cancel_of_lt', cancel_of_ne, coe_sub, eq_sub_of_add_eq, eq_sub_of_add_eq', eq_top_of_pow, exists_add_lt_of_add_lt, exists_lt_add_of_lt_add, iInf_add, iInf_add_iInf, iInf_add_iInf_of_monotone, iInf_gt_eq_self, iInf₂_add, iSup_add, iSup_add_iSup, iSup_add_iSup_le, iSup_add_iSup_of_monotone, iSup_eq_zero, iSup_lt_eq_self, iSup_natCast, iSup_sub, iSup_zero, image_coe_Icc, image_coe_Ici, image_coe_Ico, image_coe_Iic, image_coe_Iio, image_coe_Ioc, image_coe_Ioi, image_coe_Ioo, image_coe_uIcc, image_coe_uIoc, image_coe_uIoo, le_iInf_add_iInf, le_iInf₂_add_iInf₂, le_of_add_le_add_left, le_of_add_le_add_right, le_sub_iff_add_le_left, le_sub_iff_add_le_right, le_sub_of_add_le_left, le_sub_of_add_le_right, le_toReal_sub, lt_add_of_sub_lt_left, lt_add_of_sub_lt_right, lt_add_right, lt_top_of_mul_ne_top_left, lt_top_of_mul_ne_top_right, mem_Iio_self_add, mem_Ioo_self_sub_add, mul_eq_left, mul_eq_right, mul_eq_top, mul_le_mul_iff_left, mul_le_mul_iff_right, mul_le_mul_left, mul_le_mul_right, mul_left_inj, mul_left_strictMono, mul_lt_mul, mul_lt_mul_iff_left, mul_lt_mul_iff_right, mul_lt_mul_left, mul_lt_mul_left', mul_lt_mul_right, mul_lt_mul_right', mul_lt_top, mul_lt_top_iff, mul_ne_top, mul_pos, mul_pos_iff, mul_right_inj, mul_right_strictMono, mul_self_lt_top_iff, mul_sub, mul_top, mul_top', natCast_sub, not_lt_top, not_lt_zero, ofReal_iInf, ofReal_sub, pow_eq_top_iff, pow_le_pow_left, pow_le_pow_left_iff, pow_lt_pow_left, pow_lt_pow_left_iff, pow_lt_top, pow_lt_top_iff, pow_ne_top, pow_ne_top_iff, pow_ne_zero, pow_pos, pow_right_strictMono, sInf_add, sSup_add, sub_add_eq_add_sub, sub_eq_of_eq_add, sub_eq_of_eq_add', sub_eq_of_eq_add_rev, sub_eq_of_eq_add_rev', sub_eq_sInf, sub_eq_top_iff, sub_iInf, sub_iSup, sub_le_sub_iff_left, sub_lt_iff_lt_left, sub_lt_iff_lt_right, sub_lt_of_lt_add, sub_lt_of_sub_lt, sub_lt_self, sub_lt_self_iff, sub_mul, sub_ne_top, sub_ne_top_iff, sub_right_inj, sub_sub_cancel, sub_sub_sub_cancel_left, sub_top, toNNReal_add, toNNReal_iInf, toNNReal_iSup, toNNReal_sInf, toNNReal_sSup, toNNReal_sub, toReal_iInf, toReal_iSup, toReal_le_add, toReal_le_add', toReal_sInf, toReal_sSup, toReal_sub_of_le, top_mul, top_mul', top_mul_top, top_pow, top_sub, top_sub_coe | 172 |
| Total | 172 |