| Metric | Count |
|---|
DefinitionssUnionPowersetGI, sigmaEquiv, sigmaToiUnion, unionEqSigmaOfDisjoint | 4 |
TheoremsiInter_nat_add, iInter_comp, iUnion_comp, iUnion_nat_add, iInter_comp, iInter_congr, iUnion_comp, iUnion_congr, Ici_iSup, Ici_iSup₂, Ici_sSup, Iic_iInf, Iic_iInf₂, Iic_sInf, of_sUnion, of_sUnion_eq_univ, univ, biInter_and, biInter_and', biInter_const, biInter_empty, biInter_eq_iInter, biInter_ge, biInter_ge_eq_iInf, biInter_gt_eq_iInf, biInter_iUnion, biInter_insert, biInter_inter, biInter_le, biInter_le_eq_iInter, biInter_lt_eq_iInter, biInter_mono, biInter_pair, biInter_singleton, biInter_subset_biInter_left, biInter_subset_biUnion, biInter_subset_of_mem, biInter_union, biInter_univ, biUnion_and, biUnion_and', biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ, biUnion_const, biUnion_diff_biUnion_subset, biUnion_empty, biUnion_eq_iUnion, biUnion_ge, biUnion_ge_eq_iUnion, biUnion_gt_eq_iUnion, biUnion_iUnion, biUnion_insert, biUnion_le, biUnion_le_eq_iUnion, biUnion_lt_eq_iUnion, biUnion_mono, biUnion_of_singleton, biUnion_pair, biUnion_self, biUnion_singleton, biUnion_subset_biUnion_left, biUnion_union, biUnion_univ, biUnion_univ_pi, coe_snd_unionEqSigmaOfDisjoint, coe_unionEqSigmaOfDisjoint_symm_apply, compl_iInter, compl_iInter₂, compl_iUnion, compl_iUnion₂, compl_sInter, compl_sUnion, diff_iInter, diff_iUnion, directedOn_iUnion, directedOn_sUnion, disjoint_iUnion_left, disjoint_iUnion_right, disjoint_iUnion₂_left, disjoint_iUnion₂_right, disjoint_sUnion_left, disjoint_sUnion_right, exists_set_mem_of_union_eq_top, iInf_eq_dif, iInter_and, iInter_coe_set, iInter_comm, iInter_congr, iInter_congr_Prop, iInter_congr_of_surjective, iInter_const, iInter_dite, iInter_eq_compl_iUnion_compl, iInter_eq_const, iInter_eq_empty_iff, iInter_eq_if, iInter_eq_univ, iInter_exists, iInter_false, iInter_ge_eq_iInter_nat_add, iInter_iInter_eq_left, iInter_iInter_eq_or_left, iInter_iInter_eq_right, iInter_inter, iInter_inter_distrib, iInter_ite, iInter_mono, iInter_mono', iInter_mono'', iInter_of_empty, iInter_option, iInter_or, iInter_plift_down, iInter_plift_up, iInter_psigma, iInter_psigma', iInter_setOf, iInter_sigma, iInter_sigma', iInter_subset, iInter_subset_iInter₂, iInter_subset_iUnion, iInter_subset_of_subset, iInter_subtype, iInter_sum, iInter_true, iInter_union, iInter_union_of_antitone, iInter_union_of_monotone, iInter_univ, iInter₂_comm, iInter₂_congr, iInter₂_eq_empty_iff, iInter₂_mono, iInter₂_mono', iInter₂_subset, iInter₂_subset_of_subset, iInter₂_union, iUnion_and, iUnion_coe_set, iUnion_comm, iUnion_congr, iUnion_congr_Prop, iUnion_congr_of_surjective, iUnion_const, iUnion_diff, iUnion_dite, iUnion_empty, iUnion_eq_compl_iInter_compl, iUnion_eq_const, iUnion_eq_dif, iUnion_eq_empty, iUnion_eq_if, iUnion_eq_range_psigma, iUnion_eq_range_sigma, iUnion_eq_univ_iff, iUnion_exists, iUnion_false, iUnion_ge_eq_iUnion_nat_add, iUnion_iInter_ge_nat_add, iUnion_iInter_subset, iUnion_iUnion_eq_left, iUnion_iUnion_eq_or_left, iUnion_iUnion_eq_right, iUnion_image_preimage_sigma_mk_eq_self, iUnion_insert_eq_range_union_iUnion, iUnion_inter, iUnion_inter_of_antitone, iUnion_inter_of_monotone, iUnion_inter_subset, iUnion_ite, iUnion_le_nat, iUnion_mono, iUnion_mono', iUnion_mono'', iUnion_nonempty_index, iUnion_nonempty_self, iUnion_of_empty, iUnion_of_singleton, iUnion_of_singleton_coe, iUnion_option, iUnion_or, iUnion_plift_down, iUnion_plift_up, iUnion_psigma, iUnion_psigma', iUnion_range_eq_iUnion, iUnion_range_eq_sUnion, iUnion_setOf, iUnion_sigma, iUnion_sigma', iUnion_singleton_eq_range, iUnion_subset, iUnion_subset_iUnion_const, iUnion_subset_iff, iUnion_subtype, iUnion_sum, iUnion_true, iUnion_union, iUnion_union_distrib, iUnion_univ_pi, iUnion₂_comm, iUnion₂_congr, iUnion₂_eq_univ_iff, iUnion₂_inter, iUnion₂_mono, iUnion₂_mono', iUnion₂_subset, iUnion₂_subset_iUnion, iUnion₂_subset_iff, insert_iInter, insert_iUnion, inter_biInter, inter_empty_of_inter_sUnion_empty, inter_eq_iInter, inter_iInter, inter_iInter_nat_succ, inter_iUnion, inter_iUnion₂, mem_biInter, mem_biUnion, mem_iInter_of_mem, mem_iInter₂, mem_iInter₂_of_mem, mem_iUnion_of_mem, mem_iUnion₂, mem_iUnion₂_of_mem, mem_sUnion_of_mem, nonempty_biUnion, nonempty_iInter, nonempty_iInter_Ici_iff, nonempty_iInter_Iic_iff, nonempty_iInter₂, nonempty_iUnion, nonempty_of_nonempty_iUnion, nonempty_of_nonempty_iUnion_eq_univ, nonempty_of_union_eq_top_of_nonempty, nonempty_sInter, nonempty_sUnion, notMem_of_notMem_sUnion, pi_def, pi_diff_pi_subset, pi_iUnion_eq_iInter_pi, range_sigma_eq_iUnion_range, sInter_diff_singleton_univ, sInter_empty, sInter_eq_biInter, sInter_eq_compl_sUnion_compl, sInter_eq_empty_iff, sInter_eq_iInter, sInter_eq_univ, sInter_iUnion, sInter_image, sInter_image2, sInter_insert, sInter_mono, sInter_pair, sInter_range, sInter_singleton, sInter_subset_of_mem, sInter_subset_sInter, sInter_union, sInter_union_sInter, sUnion_diff_singleton_empty, sUnion_empty, sUnion_eq_biUnion, sUnion_eq_compl_sInter_compl, sUnion_eq_empty, sUnion_eq_iUnion, sUnion_eq_univ_iff, sUnion_iUnion, sUnion_image, sUnion_image2, sUnion_insert, sUnion_inter_sUnion, sUnion_mem_empty_univ, sUnion_mono, sUnion_mono_subsets, sUnion_mono_supsets, sUnion_pair, sUnion_powerset_gc, sUnion_range, sUnion_singleton, sUnion_subset, sUnion_subset_iff, sUnion_subset_sUnion, sUnion_union, setOf_exists, setOf_forall, sigmaToiUnion_bijective, sigmaToiUnion_injective, sigmaToiUnion_surjective, subset_biUnion_of_mem, subset_iInter, subset_iInter_iff, subset_iInter₂, subset_iInter₂_iff, subset_iUnion, subset_iUnion_of_subset, subset_iUnion₂, subset_iUnion₂_of_subset, subset_powerset_iff, subset_sInter, subset_sInter_iff, subset_sUnion_of_mem, subset_sUnion_of_subset, union_distrib_iInter_left, union_distrib_iInter_right, union_distrib_iInter₂_left, union_distrib_iInter₂_right, union_eq_iUnion, union_iInter, union_iInter₂, union_iUnion, union_iUnion_nat_succ, univ_pi_eq_iInter, exists_sUnion, forall_sUnion, iInf_iUnion, iInf_sUnion, iSup_iUnion, iSup_sUnion, sInf_sUnion, sSup_iUnion, sSup_sUnion | 324 |
| Total | 328 |