| Metric | Count |
|---|
Definitionscompls, diffs, disjSups, hasInfs, hasSups, «term_\\_», «term_ᶜˢ», «term_○_» | 8 |
Theoremscompls, diffs, infs, of_compls, of_diffs_left, of_diffs_right, of_disjSups_left, of_disjSups_right, of_infs_left, of_infs_right, of_sups_left, of_sups_right, sups, biUnion_image_inf_left, biUnion_image_inf_right, biUnion_image_sdiff_left, biUnion_image_sdiff_right, biUnion_image_sup_left, biUnion_image_sup_right, card_compls, card_diffs_iff, card_diffs_le, card_disjSups_le, card_infs_iff, card_infs_le, card_sups_iff, card_sups_le, coe_compls, coe_diffs, coe_infs, coe_sups, compl_mem_compls, compls_compls, compls_empty, compls_eq_empty, compls_infs, compls_infs_eq_diffs, compls_inter, compls_nonempty, compls_singleton, compls_subset_compls, compls_subset_iff, compls_sups, compls_union, compls_univ, diffs_compls_eq_infs, diffs_empty, diffs_eq_empty, diffs_inter_subset_left, diffs_inter_subset_right, diffs_nonempty, diffs_right_comm, diffs_singleton, diffs_subset, diffs_subset_iff, diffs_subset_left, diffs_subset_right, diffs_union_left, diffs_union_right, disjSups_assoc, disjSups_comm, disjSups_disjSups_disjSups_comm, disjSups_empty_left, disjSups_empty_right, disjSups_inter_subset_left, disjSups_inter_subset_right, disjSups_left_comm, disjSups_right_comm, disjSups_singleton, disjSups_subset, disjSups_subset_iff, disjSups_subset_left, disjSups_subset_right, disjSups_subset_sups, disjSups_union_left, disjSups_union_right, empty_diffs, empty_infs, empty_sups, exists_compls_iff, filter_infs_le, filter_sups_le, forall_disjSups_iff, forall_infs_iff, forall_mem_compls, forall_mem_diffs, forall_sups_iff, image_compl, image_inf_product, image_infs, image_sdiff_product, image_subset_diffs_left, image_subset_diffs_right, image_subset_infs_left, image_subset_infs_right, image_subset_sups_left, image_subset_sups_right, image_sup_product, image_sups, inf_mem_infs, infs_assoc, infs_comm, infs_compls_eq_diffs, infs_empty, infs_eq_empty, infs_infs_infs_comm, infs_inter_subset_left, infs_inter_subset_right, infs_left_comm, infs_nonempty, infs_right_comm, infs_self, infs_self_subset, infs_singleton, infs_subset, infs_subset_iff, infs_subset_left, infs_subset_right, infs_sups_subset_left, infs_sups_subset_right, infs_union_left, infs_union_right, instAssociativeDisjSups, instCommutativeDisjSups, inter_mem_infs, map_infs, map_sups, mem_compls, mem_diffs, mem_disjSups, mem_infs, mem_sups, powerset_infs_powerset_self, powerset_inter, powerset_sups_powerset_self, powerset_union, sdiff_mem_diffs, singleton_diffs, singleton_diffs_singleton, singleton_infs, singleton_infs_singleton, singleton_sups, singleton_sups_singleton, sized_compls, subset_diffs, subset_infs, subset_infs_self, subset_sups, subset_sups_self, sup_mem_sups, sups_assoc, sups_comm, sups_empty, sups_eq_empty, sups_eq_self, sups_infs_subset_left, sups_infs_subset_right, sups_inter_subset_left, sups_inter_subset_right, sups_left_comm, sups_nonempty, sups_right_comm, sups_singleton, sups_subset, sups_subset_iff, sups_subset_left, sups_subset_right, sups_subset_self, sups_sups_sups_comm, sups_union_left, sups_union_right, union_mem_sups, univ_infs_univ, univ_sups_univ, compls | 175 |
| Total | 183 |
| Name | Category | Theorems |
|---|
compls 📖 | CompOp | 29 mathmath: card_compls, sized_compls, shadow_compls, compl_mem_compls, compls_nonempty, compls_subset_iff, compls_compls, diffs_compls_eq_infs, compls_subset_compls, compls_inter, Set.Sized.compls, AhlswedeZhang.infSum_compls_add_supSum, compls_sups, compls_infs, compls_union, infs_compls_eq_diffs, compls_infs_eq_diffs, mem_compls, exists_compls_iff, coe_compls, upShadow_compls, compls_eq_empty, compl_truncatedInf, compls_empty, Nonempty.compls, image_compl, compls_singleton, compl_truncatedSup, compls_univ
|
diffs 📖 | CompOp | 33 mathmath: biUnion_image_sdiff_left, image_subset_diffs_right, biUnion_image_sdiff_right, diffs_subset_left, empty_diffs, singleton_diffs_singleton, diffs_union_right, diffs_eq_empty, singleton_diffs, card_diffs_le, image_subset_diffs_left, subset_diffs, Nonempty.diffs, diffs_compls_eq_infs, diffs_empty, card_le_card_diffs, image_sdiff_product, le_card_diffs_mul_card_diffs, diffs_inter_subset_left, diffs_nonempty, coe_diffs, infs_compls_eq_diffs, diffs_subset, compls_infs_eq_diffs, diffs_singleton, diffs_subset_iff, diffs_subset_right, mem_diffs, diffs_right_comm, card_diffs_iff, sdiff_mem_diffs, diffs_inter_subset_right, diffs_union_left
|
disjSups 📖 | CompOp | 21 mathmath: disjSups_subset_iff, disjSups_right_comm, instCommutativeDisjSups, disjSups_singleton, disjSups_comm, disjSups_subset_left, disjSups_left_comm, mem_disjSups, disjSups_subset, disjSups_inter_subset_right, disjSups_disjSups_disjSups_comm, disjSups_assoc, card_disjSups_le, disjSups_empty_right, disjSups_union_left, disjSups_empty_left, disjSups_subset_sups, disjSups_subset_right, disjSups_union_right, instAssociativeDisjSups, disjSups_inter_subset_left
|
hasInfs 📖 | CompOp | 59 mathmath: image_subset_infs_left, univ_infs_univ, infs_nonempty, truncatedSup_infs, coe_infs, infs_comm, inter_mem_infs, AhlswedeZhang.supSum_union_add_supSum_infs, sups_infs_subset_left, infs_sups_subset_right, powerset_infs_powerset_self, singleton_infs, infs_infs_infs_comm, infs_subset_left, filter_infs_le, diffs_compls_eq_infs, infs_eq_empty, empty_infs, infs_self, card_infs_le, infs_left_comm, sups_infs_subset_right, singleton_infs_singleton, compls_sups, image_infs, image_subset_infs_right, compls_infs, powerset_inter, infs_singleton, biUnion_image_inf_right, le_card_infs_mul_card_sups, infs_compls_eq_diffs, infs_union_right, infs_right_comm, compls_infs_eq_diffs, infs_assoc, card_infs_iff, infs_empty, map_infs, collapse_modular, mem_infs, Nonempty.infs, infs_sups_subset_left, infs_self_subset, truncatedSup_infs_of_notMem, infs_subset, infs_inter_subset_left, biUnion_image_inf_left, infs_subset_right, infs_subset_iff, subset_infs, infs_inter_subset_right, inf_mem_infs, four_functions_theorem, infs_union_left, subset_infs_self, four_functions_theorem, card_truncatedSup_union_add_card_truncatedSup_infs, image_inf_product
|
hasSups 📖 | CompOp | 57 mathmath: sups_inter_subset_right, subset_sups, powerset_sups_powerset_self, card_sups_iff, sups_infs_subset_left, univ_sups_univ, singleton_sups_singleton, image_subset_sups_left, infs_sups_subset_right, sups_singleton, sups_assoc, sups_subset_right, image_subset_sups_right, sups_eq_empty, sups_empty, coe_sups, sups_union_right, union_mem_sups, sups_right_comm, sup_mem_sups, empty_sups, sups_union_left, sups_left_comm, card_truncatedInf_union_add_card_truncatedInf_sups, truncatedInf_sups_of_notMem, sups_infs_subset_right, sups_subset_self, compls_sups, sups_nonempty, biUnion_image_sup_right, compls_infs, filter_sups_le, image_sup_product, sups_subset_left, le_card_infs_mul_card_sups, biUnion_image_sup_left, sups_comm, map_sups, card_sups_le, sups_sups_sups_comm, sups_subset_iff, truncatedInf_sups, subset_sups_self, sups_eq_self, collapse_modular, singleton_sups, sups_subset, Nonempty.sups, image_sups, powerset_union, disjSups_subset_sups, infs_sups_subset_left, sups_inter_subset_left, mem_sups, four_functions_theorem, AhlswedeZhang.infSum_union_add_infSum_sups, four_functions_theorem
|