| Metric | Count |
|---|
DefinitionsdecidableMemIcc, decidableMemIci, decidableMemIco, decidableMemIic, decidableMemIio, decidableMemIoc, decidableMemIoi, decidableMemIoo, instIccUnique | 9 |
TheoremsIci_eq, Ici_eq, Ioi_eq, Iic_eq, Iio_eq, Iic_eq, Icc_bot, Icc_bot_top, Icc_diff_Ico_same, Icc_diff_Ioc_same, Icc_diff_Ioo_same, Icc_diff_both, Icc_diff_left, Icc_diff_right, Icc_eq_Icc_iff, Icc_eq_Ico_same_iff, Icc_eq_Ioc_same_iff, Icc_eq_Ioo_same_iff, Icc_eq_empty, Icc_eq_empty_iff, Icc_eq_empty_of_lt, Icc_eq_singleton_iff, Icc_inter_Icc, Icc_inter_Icc_eq_singleton, Icc_ofDual, Icc_prod_Icc, Icc_prod_eq, 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_iff, Icc_subset_Ici_self, Icc_subset_Ico_iff, Icc_subset_Ico_right, Icc_subset_Iic_iff, Icc_subset_Iic_self, Icc_subset_Iio_iff, Icc_subset_Ioc_iff, Icc_subset_Ioi_iff, Icc_subset_Ioo, Icc_subset_Ioo_iff, Icc_toDual, Icc_top, Ici_False, Ici_True, Ici_bot, Ici_diff_Ioi_same, Ici_diff_left, Ici_inj, Ici_injective, Ici_inter_Ici, Ici_inter_Iic, Ici_inter_Iio, Ici_ofDual, Ici_prod_Ici, Ici_prod_eq, Ici_ssubset_Ici, Ici_subset_Ici, Ici_subset_Ioi, Ici_toDual, Ici_top, Ico_bot, Ico_diff_Ioo_same, Ico_diff_left, Ico_eq_Icc_same_iff, Ico_eq_Ioc_same_iff, Ico_eq_Ioo_same_iff, Ico_eq_empty, Ico_eq_empty_iff, Ico_eq_empty_of_le, Ico_insert_right, Ico_inter_Ici, Ico_ofDual, Ico_self, Ico_subset_Icc_self, Ico_subset_Ici_self, Ico_subset_Ico, Ico_subset_Ico_left, Ico_subset_Ico_right, Ico_subset_Iio_self, Ico_subset_Ioo_left, Ico_toDual, Ico_union_right, Iic_False, Iic_True, Iic_bot, Iic_diff_Iio_same, Iic_diff_right, Iic_inj, Iic_injective, Iic_inter_Ici, Iic_inter_Iic, Iic_inter_Ioc_of_le, Iic_inter_Ioi, Iic_ofDual, Iic_prod_Iic, Iic_prod_eq, Iic_ssubset_Iic, Iic_subset_Iic, Iic_subset_Iio, Iic_toDual, Iic_top, Iio_False, Iio_True, Iio_bot, Iio_eq_empty_iff, Iio_insert, Iio_inter_Ici, Iio_inter_Ioi, Iio_nonempty, Iio_ofDual, Iio_ssubset_Iic_self, Iio_ssubset_Iio, Iio_subset_Iic, Iio_subset_Iic_self, Iio_subset_Iio, Iio_toDual, Iio_top, Iio_union_right, Ioc_diff_Ioo_same, Ioc_diff_right, Ioc_eq_Icc_same_iff, Ioc_eq_Ico_same_iff, Ioc_eq_Ioo_same_iff, Ioc_eq_empty, Ioc_eq_empty_iff, Ioc_eq_empty_of_le, Ioc_insert_left, Ioc_inter_Iic, Ioc_ofDual, Ioc_self, Ioc_subset_Icc_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_toDual, Ioc_top, Ioc_union_left, Ioi_False, Ioi_True, Ioi_bot, Ioi_eq_empty_iff, Ioi_insert, Ioi_inter_Iic, Ioi_inter_Iio, Ioi_nonempty, Ioi_ofDual, Ioi_ssubset_Ici_self, Ioi_ssubset_Ioi, Ioi_subset_Ici, Ioi_subset_Ici_self, Ioi_subset_Ioi, Ioi_toDual, Ioi_top, Ioi_union_left, Ioo_eq_Icc_same_iff, Ioo_eq_Ico_same_iff, Ioo_eq_Ioc_same_iff, Ioo_eq_empty, Ioo_eq_empty_iff, Ioo_eq_empty_of_le, Ioo_insert_left, Ioo_insert_right, Ioo_ofDual, Ioo_self, Ioo_subset_Icc_self, Ioo_subset_Ico_self, Ioo_subset_Iio_self, Ioo_subset_Ioc_self, Ioo_subset_Ioi_self, Ioo_subset_Ioo, Ioo_subset_Ioo_left, Ioo_subset_Ioo_right, Ioo_toDual, Ioo_union_both, Ioo_union_left, Ioo_union_right, eq_endpoints_or_mem_Ioo_of_mem_Icc, eq_left_or_mem_Ioo_of_mem_Ico, eq_right_or_mem_Ioo_of_mem_Ioc, instNoMaxOrderElemIci, instNoMaxOrderElemIoi, instNoMinOrderElemIic, instNoMinOrderElemIio, left_mem_Icc, left_mem_Ici, left_mem_Ico, left_mem_Ioc, left_mem_Ioo, left_notMem_Ioc, left_notMem_Ioo, mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset, mem_Icc_of_Ico, mem_Icc_of_Ioc, mem_Icc_of_Ioo, mem_Ici_Ioi_of_subset_of_subset, mem_Ici_of_Ioi, mem_Ico_of_Ioo, mem_Iic_Iio_of_subset_of_subset, mem_Iic_of_Iio, mem_Ioc_of_Ioo, nonempty_Icc, nonempty_Icc_subtype, nonempty_Ici, nonempty_Ici_subtype, nonempty_Ico, nonempty_Ico_subtype, nonempty_Iic, nonempty_Iic_subtype, nonempty_Iio, nonempty_Iio_subtype, nonempty_Ioc, nonempty_Ioc_subtype, nonempty_Ioi, nonempty_Ioi_subtype, nonempty_Ioo, nonempty_Ioo_subtype, notMem_Icc_of_gt, notMem_Icc_of_lt, notMem_Ico_of_ge, notMem_Ico_of_lt, notMem_Iio_self, notMem_Ioc_of_gt, notMem_Ioc_of_le, notMem_Ioi_self, notMem_Ioo_of_ge, notMem_Ioo_of_le, right_mem_Icc, right_mem_Ico, right_mem_Iic, right_mem_Ioc, right_mem_Ioo, right_notMem_Ico, right_notMem_Ioo, self_mem_Ici, self_mem_Iic, self_notMem_Iio, self_notMem_Ioi, subsingleton_Icc_iff, subsingleton_Icc_of_ge, instNoMaxOrderElemIco, instNoMaxOrderElemIio, instNoMaxOrderElemIoo, instNoMinOrderElemIoc, instNoMinOrderElemIoi, instNoMinOrderElemIoo | 253 |
| Total | 262 |