| Metric | Count |
|---|
DefinitionsIicFinsetSet, instUniqueSubtypeMemIicBot, fintypeOfMemBounds | 3 |
Theoremsfinite, finite, nonempty_Icc_of_le, nonempty_Ico_of_lt, nonempty_Iio_of_not_isMin, nonempty_Ioc_of_lt, nonempty_Ioi_of_not_isMax, Icc_bot, Icc_bot_top, Icc_diff_Ico_self, Icc_diff_Ioc_self, Icc_diff_Ioo_self, Icc_diff_both, Icc_eq_cons_Ico, Icc_eq_cons_Ioc, Icc_eq_empty, Icc_eq_empty_iff, Icc_eq_empty_of_lt, Icc_eq_singleton_iff, Icc_erase_left, Icc_erase_right, Icc_filter_lt_of_lt_right, Icc_map_sectL, Icc_map_sectR, Icc_min_max, Icc_self, Icc_ssubset_Icc_left, Icc_ssubset_Icc_right, Icc_subset_Icc, Icc_subset_Icc_iff, Icc_subset_Icc_left, Icc_subset_Icc_right, Icc_subset_Ici_self, Icc_subset_Ico_iff, Icc_subset_Ico_right, Icc_subset_Iic_self, Icc_subset_Ioc_iff, Icc_subset_Ioo_iff, Icc_subset_uIcc, Icc_subset_uIcc', Icc_top, Ici_bot, Ici_eq_cons_Ioi, Ici_erase, Ici_ssubset_Ici, Ici_subset_Ici, Ici_top, Ico_bot, Ico_diff_Ico_left, Ico_diff_Ico_right, Ico_diff_Ioo_self, Ico_disjoint_Ico_consecutive, Ico_eq_cons_Ioo, Ico_eq_empty, Ico_eq_empty_iff, Ico_eq_empty_of_le, Ico_erase_left, Ico_filter_le, Ico_filter_le_left, Ico_filter_le_of_le_left, Ico_filter_le_of_left_le, Ico_filter_le_of_right_le, Ico_filter_lt, Ico_filter_lt_of_le_left, Ico_filter_lt_of_le_right, Ico_filter_lt_of_right_le, Ico_insert_right, Ico_inter_Ico, Ico_inter_Ico_consecutive, Ico_map_sectL, Ico_map_sectR, Ico_self, Ico_subset_Icc_self, Ico_subset_Ici_self, Ico_subset_Ico, Ico_subset_Ico_iff, Ico_subset_Ico_left, Ico_subset_Ico_right, Ico_subset_Ico_union_Ico, Ico_subset_Iic_self, Ico_subset_Iio_self, Ico_subset_Ioo_left, Ico_union_Ico, Ico_union_Ico', Ico_union_Ico_eq_Ico, Iic_bot, Iic_diff_Ioc, Iic_diff_Ioc_self_of_le, Iic_disjoint_Ioc, Iic_eq_cons_Iio, Iic_erase, Iic_filter_lt_of_lt_right, Iic_ssubset_Iic, Iic_subset_Iic, Iic_top, Iic_union_Ioc_eq_Iic, Iio_bot, Iio_eq_empty, Iio_filter_lt, Iio_insert, Iio_nonempty, Iio_ssubset_Iio, Iio_subset_Iic_self, Iio_subset_Iio, Ioc_diff_Ioo_self, Ioc_disjoint_Ioc, Ioc_disjoint_Ioc_of_le, Ioc_eq_cons_Ioo, Ioc_eq_empty, Ioc_eq_empty_iff, Ioc_eq_empty_of_le, Ioc_erase_right, Ioc_filter_lt_of_lt_right, Ioc_insert_left, Ioc_inter_Ioc, Ioc_map_sectL, Ioc_map_sectR, Ioc_self, Ioc_subset_Icc_self, Ioc_subset_Ici_self, Ioc_subset_Iic_self, Ioc_subset_Ioc, Ioc_subset_Ioc_left, Ioc_subset_Ioc_right, Ioc_subset_Ioi_self, Ioc_subset_Ioo_right, Ioc_top, Ioc_union_Ioc_eq_Ioc, Ioi_disjUnion_Iio, Ioi_eq_empty, Ioi_insert, Ioi_nonempty, Ioi_ssubset_Ioi, Ioi_subset_Ici_self, Ioi_subset_Ioi, Ioi_top, Ioo_eq_empty, Ioo_eq_empty_iff, Ioo_eq_empty_of_le, Ioo_filter_lt, Ioo_insert_left, Ioo_insert_right, Ioo_map_sectL, Ioo_map_sectR, Ioo_self, Ioo_subset_Icc_self, Ioo_subset_Ici_self, Ioo_subset_Ico_self, Ioo_subset_Iic_self, Ioo_subset_Iio_self, Ioo_subset_Ioc_self, Ioo_subset_Ioi_self, Ioo_subset_Ioo, Ioo_subset_Ioo_left, Ioo_subset_Ioo_right, card_Ico_eq_card_Icc_sub_one, card_Iio_eq_card_Iic_sub_one, card_Ioc_eq_card_Icc_sub_one, card_Ioi_eq_card_Ici_sub_one, card_Ioo_eq_card_Icc_sub_two, card_Ioo_eq_card_Ico_sub_one, card_Ioo_eq_card_Ioc_sub_one, disjoint_Ioi_Iio, eq_of_mem_uIcc_of_mem_uIcc, eq_of_mem_uIcc_of_mem_uIcc', filter_ge_eq_Iic, filter_gt_eq_Iio, filter_le_eq_Ici, filter_le_le_eq_Icc, filter_le_lt_eq_Ico, filter_lt_eq_Ioi, filter_lt_le_eq_Ioc, filter_lt_lt_eq_Ioo, image_subset_Iic_sup, inf'_Ici, inf_Ici, left_mem_Icc, left_mem_Ico, left_mem_uIcc, left_notMem_Ioc, left_notMem_Ioo, mem_uIcc', mem_uIcc_of_ge, mem_uIcc_of_le, nonempty_Icc, nonempty_Ici, nonempty_Ico, nonempty_Iic, nonempty_Iio, nonempty_Ioc, nonempty_Ioi, nonempty_Ioo, nonempty_uIcc, notMem_Iio_self, notMem_Ioi_self, notMem_uIcc_of_gt, notMem_uIcc_of_lt, right_mem_Icc, right_mem_Ioc, right_mem_uIcc, right_notMem_Ico, right_notMem_Ioo, subset_Iic_sup_id, sup'_Iic, sup_Iic, uIcc_comm, uIcc_eq_union, uIcc_injective_left, uIcc_injective_right, uIcc_map_sectL, uIcc_map_sectR, uIcc_of_ge, uIcc_of_le, uIcc_of_not_ge, uIcc_of_not_le, uIcc_self, uIcc_subset_Icc, uIcc_subset_uIcc, uIcc_subset_uIcc_iff_le, uIcc_subset_uIcc_iff_le', uIcc_subset_uIcc_iff_mem, uIcc_subset_uIcc_left, uIcc_subset_uIcc_right, uIcc_subset_uIcc_union_uIcc, uIcc_toDual, finsetIoi_eq, finsetIio_eq, exists_gt, exists_lt, not_bddAbove, not_bddBelow, infinite_iff_exists_gt, infinite_iff_exists_lt, antitone_iff_forall_covBy, antitone_iff_forall_wcovBy, le_iff_reflTransGen_covBy, le_iff_transGen_wcovBy, lt_iff_transGen_covBy, monotone_iff_forall_covBy, monotone_iff_forall_wcovBy, not_lt_of_denselyOrdered_of_locallyFinite, strictAnti_iff_forall_covBy, strictMono_iff_forall_covBy, transGen_covBy_of_lt, transGen_wcovBy_of_le | 245 |
| Total | 248 |