| Name | Category | Theorems |
|---|
instDistribLattice 📖 | CompOp | — |
instInter 📖 | CompOp | 240 mathmath: expect_ite_mem, empty_inter, mul_inter_subset, insert_inter_of_notMem, OrderEmbedding.birkhoffFinset_inf, sum_ite_mem, inter_erase, inter_union_distrib_right, inter_sdiff_assoc, image₂_inter_singleton, sum_union_inter, inter_inter_distrib_left, affineCombination_apply_eq_lineMap_sum, compl_inter, IsLowerSet.le_card_inter_finset, inter_subset_ite, image₂_inter_right, inter_sub_union_subset_union, dens_inter_add_dens_sdiff, image_inter_of_injOn, inter_eq_inter_iff_left, inter_self, inter_subset_right, smul_finset_inter, dens_sdiff_add_dens_inter, Finsupp.support_mul, inter_union_self, inter_mem_infs, inter_filter, sups_inter_subset_right, union_inter_distrib_left, dens_union_add_dens_inter, IsLowerSet.card_inter_le_finset, compl_union, card_inter, neg_inter, product_inter, sum_indicator_eq_sum_inter, mulDysonETransform_snd, inter_sdiff_self, inter_singleton_of_mem, inter_vadd_subset, card_sdiff, inter_sub_subset, sum_card_inter, erase_inter_comm, inter_subset_inter_right, nonMemberSubfamily_inter, inter_comm, inter_compl, sum_piecewise, cast_card_union, card_union, union_vadd_inter_subset_union, vadd_inter_subset, IsLowerSet.le_card_inter_finset', card_singleton_inter, image₂_inter_union_subset, Ico_inter_Ico_consecutive, inter_left_comm, image_inter, inter_eq_inter_iff_right, Shatters.subset_iff, inter_subset_inter, vadd_finset_inter, sum_inter_add_sum_diff, memberSubfamily_inter, sum_card_inter_le, addDysonETransform_snd, insert_inter_of_mem, inter_vsub_subset, smul_finset_inter_subset, Ico_inter_Ico, disjoint_or_nonempty_inter, inf_eq_inter, sdiff_inter_self, inter_eq_univ, card_sdiff_add_card_inter, singleton_inter_of_notMem, DFinsupp.support_inf, add_inter_subset, Ioc_inter_Ioc, Nat.primeFactors_gcd, not_disjoint_iff_nonempty_inter, IsUpperSet.le_card_inter_finset, inter_inter_inter_comm, inf_eq_inter', disjSups_inter_subset_right, sdiff_inter_distrib_right, inter_subset_union, inter_union_distrib_left, singleton_mul_inter, pimage_inter, card_union_add_card_inter, Shatters.exists_inter_eq_singleton, card_inter_vadd, sym_inter, inter_smul_union_subset_union, filter_inter, inter_right_idem, inter_sdiff_left_comm, singleton_add_inter, compls_inter, image₂_union_inter_subset_union, card_smul_inter, sdiff_eq_sdiff_iff_inter_eq_inter, SimpleGraph.exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite, diffs_inter_subset_left, image₂_inter_union_subset_union, card_inter_add_card_sdiff, Set.toFinset_inter, SimpleGraph.IsFiveWheelLike.card_inter, image₂_inter_subset_right, singleton_inter_of_mem, SimpleGraph.map_neighborFinset_induce, image_inter_subset, card_inter_add_card_union, disjoint_iff_inter_eq_empty, inter_singleton_of_notMem, le_sum_card_inter, sub_inter_subset, inter_val_nd, SimpleGraph.sdiff_compl_neighborFinset_inter_eq, inter_singleton, union_mul_inter_subset, inter_assoc, prod_ite_mem, inter_mul_union_subset, inter_mul_union_subset_union, inv_inter, filter_and, biUnion_inter, fold_union_inter, sdiff_inter_self_right, inter_add_singleton, powerset_inter, dens_inter_add_dens_union, inter_insert_of_notMem, image₂_inter_subset_left, inter_right_comm, image₂_union_inter_subset, insert_inter_distrib, inter_pow_subset, inter_biUnion, inter_smul_subset, inter_div_union_subset_union, sdiff_sdiff_self_left, Set.Finite.toFinset_inter, inter_eq_right, card_inter_smul, vadd_finset_inter_subset, addETransformRight_snd, inter_nsmul_subset, image₂_inter_left, diag_inter, List.toFinset_inter, inter_insert, union_add_inter_subset, prod_inter_mul_prod_diff, univ_inter, inter_eq_left, inter_nonempty_of_card_lt_card_add_card, eraseNone_inter, disjoint_sdiff_inter, addETransformLeft_fst, card_smul_inter_smul, mem_inter_of_mem, shatters_iff, Multiset.toFinset_inter, singleton_inter, mulETransformRight_snd, div_inter_subset, union_mul_inter_subset_union, inter_univ, subset_inter_iff, inter_left_idem, SimpleGraph.compl_neighborFinset_sdiff_inter_eq, union_add_inter_subset_union, subset_inter, prod_mulIndicator_eq_prod_inter, union_sub_inter_subset_union, union_inter_cancel_left, smul_finset_inter₀, card_vadd_inter, sdiff_inter_right_comm, inter_add_union_subset_union, smul_inter_subset, inter_vadd_union_subset_union, mem_inter, sdiff_inter_self_left, inter_val, coe_inter, Finsupp.support_inf, inter_mul_singleton, sups_inter_subset_left, union_eq_sdiff_union_sdiff_union_inter, inter_subset_inter_left, IsUpperSet.card_inter_le_finset, erase_inter, infs_inter_subset_left, filter_mem_eq_inter, inter_product, union_smul_inter_subset_union, map_inter, union_inter_distrib_right, prod_piecewise, inter_insert_of_mem, inter_div_subset, product_inter_product, inter_subset_left, inter_add_subset, offDiag_inter, union_inter_cancel_right, range_inter_range, inter_empty, SimpleGraph.edgeFinset_inf, infs_inter_subset_right, sdiff_union_inter, toLeft_inter, prod_union_inter, card_vadd_inter_vadd, sdiff_union_distrib, SimpleGraph.map_edgeFinset_induce, sdiff_eq_inter_compl, image₂_singleton_inter, mulETransformLeft_fst, diffs_inter_subset_right, disjSups_inter_subset_left, filter_inter_distrib, inter_mul_subset, preimage_inter, union_div_inter_subset_union, toRight_inter, YoungDiagram.cells_inf, cast_card_inter, inter_add_union_subset, vsub_inter_subset, sdiff_sdiff_left', inter_inter_distrib_right, insert_inter
|
instLattice 📖 | CompOp | 130 mathmath: Finpartition.ofExistsUnique_parts, sup_singleton_eq_self, Finpartition.IsEquipartition.filter_ne_average_add_one_eq_average, Equiv.Perm.support_prod_of_pairwise_disjoint, bind_def, Finpartition.equitabilise_aux, SzemerediRegularity.a_add_one_le_four_pow_parts_card, sup_eq_union', Finpartition.card_filter_equitabilise_big, Finpartition.IsEquipartition.card_biUnion_offDiag_le', symmDiff_eq_union_iff, Colex.toColex_lt_toColex_iff_max'_mem, Set.toFinset_symmDiff, mem_sup, SimpleGraph.regularityReduced_adj, Finpartition.IsEquipartition.card_large_parts_eq_mod, Finpartition.indiscrete_isEquipartition, Colex.le_iff_max'_mem, inclusion_exclusion_card_inf_compl, inter_mem_infs, Finpartition.parts_bot, Finpartition.mk_mem_nonUniforms, Rel.card_interedges_finpartition, Multiset.support_sum_subset, support_sum_subset, Finpartition.isEquipartition_iff_card_parts_eq_average, SupIndep.sup, Colex.toColex_le_toColex_iff_max'_mem, AhlswedeZhang.supSum_union_add_supSum_infs, powerset_sups_powerset_self, smul_finset_symmDiff, exists_birkhoff_representation, seq_def, Finpartition.card_parts_le_card, Finpartition.bot_isUniform, Finpartition.top_isEquipartition, Multiset.mem_sup_map_support_iff, Finpartition.card_nonuniformWitnesses_le, vadd_finset_symmDiff, SimpleGraph.IsTuranMaximal.card_parts_le, Rel.card_interedges_finpartition_right, powerset_infs_powerset_self, Finpartition.IsEquipartition.sum_nonUniforms_lt', Finpartition.exists_mem, inclusion_exclusion_sum_inf_compl, inf_eq_inter, Finpartition.mem_atomise, symmDiff_nonempty, Finpartition.IsEquipartition.card_small_parts_eq_mod, smul_finset_symmDiff₀, Set.Finite.toFinset_symmDiff, inf_eq_inter', mem_sup_support_iff, Finpartition.part_mem, Finpartition.exists_enumeration, Finpartition.mem_part_iff_exists, symmDiff_subset_sdiff, union_mem_sups, symmDiff_subset_union, Finpartition.exists_equipartition_card_eq, Equiv.Perm.support_mul_le, Finpartition.card_atomise_le, inclusion_exclusion_card_biUnion, fold_sup_bot_singleton, sup_eq_biUnion, szemeredi_regularity, Finpartition.coe_energy, Finpartition.biUnion_parts, Finpartition.empty_notMem_parts, Finpartition.card_mod_card_parts_le, SimpleGraph.unreduced_edges_subset, card_truncatedInf_union_add_card_truncatedInf_sups, List.zipWith_swap_prod_support', List.support_sum_eq, List.mem_foldr_sup_support_iff, Finpartition.mem_bot_iff, Finpartition.ofSetoid_parts_val, sup_singleton_apply, coe_symmDiff, mem_sup', Finpartition.card_filter_atomise_le_two_pow, mem_inf, powerset_inter, Equiv.Perm.support_prod_le, Finpartition.nonempty_of_not_uniform, Colex.lt_iff_max'_mem, symmDiff_subset_sdiff', Multiset.support_sum_eq, inclusion_exclusion_sum_biUnion, List.support_sum_subset, Finpartition.existsUnique_mem, Finpartition.card_filter_equitabilise_small, powersetCard_sup, Finpartition.card_bot, Finpartition.card_parts_equitabilise, support_sum_eq, mem_inf', Finpartition.nonUniforms_bot, SimpleGraph.IsTuranMaximal.card_parts, Finpartition.mk_mem_sparsePairs, Finpartition.IsEquipartition.exists_partsEquiv, LatticeHom.birkhoffFinset_injective, symmDiff_eq_empty, Rel.card_interedges_finpartition_left, SzemerediRegularity.coe_m_add_one_pos, collapse_modular, mem_symmDiff, SSet.stdSimplex.face_inter_face, Finpartition.sum_card_parts, powerset_union, sym_succ, sup_toFinset, List.zipWith_swap_prod_support, sup_eq_union, Finpartition.IsEquipartition.exists_partPreservingEquiv, MvPolynomial.support_symmDiff_support_subset_support_add, Finpartition.biUnion_filter_atomise, symmDiff_eq_union, AhlswedeZhang.infSum_union_add_infSum_sups, disjiUnion_Iic_disjointed, Finpartition.not_isEquipartition, Finpartition.bot_isEquipartition, Finpartition.part_surjOn, Finpartition.exists_subset_part_bijOn, four_functions_theorem, card_truncatedSup_union_add_card_truncatedSup_infs, image_symmDiff, Finpartition.IsEquipartition.card_interedges_sparsePairs_le', Finpartition.atomise_empty, Finpartition.ofSetSetoid_parts
|
instUnion 📖 | CompOp | 354 mathmath: min'_union, DFinsupp.support_zipWith, dens_union_of_disjoint, union_subset, max_union, MvPolynomial.coeffs_add, Set.toFinset_union, inter_union_distrib_right, union_union_distrib_right, sum_union_inter, Finsupp.card_Ioc, product_union, Ico_subset_Ico_union_Ico, truncatedSup_union_of_notMem, compl_inter, Finsupp.card_Ico, union_mul, Icc_eq_image_powerset, inter_sub_union_subset_union, uIcc_eq_union, insert_eq, diag_union, sup_eq_union', Ioc_union_Ioc_eq_Ioc, Icc_succ_succ, disjoint_union_right, Multiset.card_Ico, MvPolynomial.vars_sub_of_disjoint, range_union_range, symmDiff_eq_union_iff, union_sdiff_self_eq_union, add_union, nonMemberSubfamily_union, prod_union_eq_left, ite_subset_union, MeasureTheory.inter_cylinder, powerset_insert, min_union, union_compl, List.toFinset_append, inter_union_self, exists_disjoint_union_of_even_card, MeasureTheory.volume_preserving_piFinsetUnion, sdiff_sdiff_eq_sdiff_union, empty_union, union_inter_distrib_left, dens_union_add_dens_inter, compl_union, card_inter, Function.update_updateFinset, union_comm, DFinsupp.zipWith_def, union_product, SimpleGraph.IsSRGWith.card_neighborFinset_union_eq, MeasureTheory.cylinder_eq_cylinder_union, Turing.TM2to1.trStmts₁_run, union_assoc, range_add, union_eq_left, AhlswedeZhang.supSum_union_add_supSum_infs, Ico_union_Ico', MeasureTheory.union_cylinder, Iic_union_Ioc_eq_Iic, instCommutativeUnion, inf_union, diffs_union_right, eraseNone_union, MvPolynomial.support_add, image₂_insert_left, Turing.PartrecToTM2.supports_union, truncatedInf_union, cast_card_union, card_union, SimpleGraph.edgeFinset_replaceVertex_of_adj, Equiv.Finset.union_inl, union_vadd_inter_subset_union, pimage_union, union_subset_union, image₂_inter_union_subset, Multiset.toFinset_add, diag_union_offDiag, Turing.PartrecToTM2.codeSupp_tail, addRothNumber_union_le, union_sub, SimpleGraph.neighborFinset_subset_between_union, Finsupp.support_add_eq, truncatedInf_union_of_notMem, erase_union_of_mem, truncatedInf_union_left, Multiset.card_Ioc, union_nonempty, sdiff_union_sdiff_cancel, offDiag_union, SimpleGraph.edgeFinset_replaceVertex_of_not_adj, vadd_union, MvPolynomial.vars_sub_subset, Equiv.Perm.Disjoint.support_mul, union_subset_union_left, union_sdiff_cancel_left, union_left_idem, image_union, SimpleGraph.neighborFinset_subset_between_union_compl, MeasureTheory.lmarginal_union, union_val_nd, insert_union, sym_union, Finsupp.card_Icc, Multiset.card_uIcc, prod_union, right_eq_union, DFinsupp.support_rangeIcc_subset, Finsupp.card_uIcc, smul_union, Finsupp.card_Ioo, sups_union_right, card_union_eq_card_add_card, SimpleGraph.edgeFinset_sup, set_biInter_inter, SkewPolynomial.support_add, Nonempty.inl, union_sdiff_right, dens_sdiff_add_dens, subset_union_left, Ioc_succ_succ, union_idempotent, sdiff_inter_distrib_right, filter_union_right, sum_union, fold_union_empty_singleton, inter_subset_union, inter_union_distrib_left, sdiff_union_self_eq_union, DFinsupp.card_Ioo, union_div, union_add, Ico_eq_image_ssubsets, MeasureTheory.disjoint_cylinder_iff, union_mem_sups, subset_union_elim, union_insert, card_union_add_card_inter, Polynomial.support_add, UniqueFactorizationMonoid.primeFactors_mul_eq_union, biUnion_union, union_sdiff_self, symmDiff_subset_union, union_vsub, addDysonETransform_fst, singleton_union, inter_smul_union_subset_union, Ico_union_Ico_eq_Ico, memberSubfamily_union_nonMemberSubfamily, DFinsupp.Icc_eq, sdiff_union_of_subset, Turing.PartrecToTM2.codeSupp_zero, union_self, filter_union_filter_not_eq, card_union_le, sdiff_union_erase_cancel, MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset, Function.updateFinset_updateFinset, image₂_union_inter_subset_union, Ico_succ_succ, union_eq_empty, mem_union_of_disjoint, truncatedSup_union, Turing.PartrecToTM2.codeSupp_fix, prod_union_eq_right, sups_union_left, SkewMonoidAlgebra.support_add, union_sdiff_distrib, SimpleGraph.unreduced_edges_subset, mulDysonETransform_fst, vsub_union, card_truncatedInf_union_add_card_truncatedInf_sups, union_smul, BoxIntegral.Prepartition.sum_disj_union_boxes, Ico_union_Ico, vadd_finset_union, image₂_inter_union_subset_union, DFinsupp.card_uIcc, Turing.PartrecToTM2.contSupp_cons₂, SupIndep.union, sup_union, gcd_union, biUnion_insert, max'_union, image₂_union_left, iInf_union, truncatedSup_union_left, slice_union_shadow_falling_succ, card_inter_add_card_union, offDiag_insert, truncatedSup_union_right, insert_union_comm, union_right_idem, union_subset_union_right, union_eq_right, smul_finset_union, SimpleGraph.sdiff_compl_neighborFinset_inter_eq, union_empty, SimpleGraph.IsSRGWith.card_neighborFinset_union_of_not_adj, union_biUnion, union_mul_inter_subset, inter_mul_union_subset, inter_mul_union_subset_union, left_eq_union, notMem_union, DFinsupp.support_sup_union_support_inf, erase_union_distrib, fold_union_inter, image_diag_union_image_offDiag, union_right_comm, Multiset.toFinset_union, insert_union_distrib, Turing.PartrecToTM2.codeSupp_succ, Turing.PartrecToTM2.codeSupp_case, dens_inter_add_dens_union, filter_or, instIdempotentOpUnion, image₂_union_inter_subset, BoxIntegral.Prepartition.disjUnion_boxes, mem_shadow_iterate_iff_exists_card, SimpleGraph.IsSRGWith.card_neighborFinset_union_of_adj, compls_union, inter_div_union_subset_union, MvPolynomial.vars_mul, YoungDiagram.cells_sup, union_left_comm, infs_union_right, DFinsupp.card_Ico, instAssociativeUnion, exists_disjoint_union_of_even_card_iff, sym2_insert, union_sdiff_symm, Finsupp.support_add, union_eq_union_iff_right, Finsupp.support_inf_union_support_sup, MeasureTheory.measurePreserving_piFinsetUnion, mulETransformRight_fst, union_sdiff_cancel_right, BoxIntegral.TaggedPrepartition.disjUnion_boxes, FreeAbelianGroup.support_add, Ioo_succ_succ, range_add_eq_union, union_add_inter_subset, union_val, addETransformLeft_snd, BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes, DFinsupp.support_add, sum_union_eq_right, MvPolynomial.support_sub, sup'_union, set_biUnion_union, mem_union, union_eq_union_iff_left, union_sdiff_of_subset, Finsupp.Icc_eq, lcm_union, Equiv.Finset.union_inr, Finsupp.rangeIcc_support, union_mul_inter_subset_union, Finmap.keys_union, Nat.primeFactors_mul, filter_union, union_union_union_comm, Multiset.card_Icc, disjoint_union_left, sub_union, SimpleGraph.compl_neighborFinset_sdiff_inter_eq, union_add_inter_subset_union, image₂_insert_right, union_erase_of_mem, union_sub_inter_subset_union, union_inter_cancel_left, Finsupp.support_sup, toLeft_union, disjSups_union_left, Turing.PartrecToTM2.codeSupp_cons, FreeMonoid.symbols_mul, inter_add_union_subset_union, FreeAddMonoid.symbols_add, filter_union_filter_neg_eq, disjUnion_eq_union, mem_union_right, mem_union_left, powerset_union, union_singleton, inter_vadd_union_subset_union, Finsupp.support_sup_union_support_inf, Equiv.Perm.Disjoint.cycleFactorsFinset_mul_eq_union, image₂_union_right, sup_eq_union, DFinsupp.support_inf_union_support_sup, sum_union_eq_left, card_union_of_disjoint, MvPolynomial.vars_add_subset, union_sdiff_left, union_eq_sdiff_union_sdiff_union_inter, map_union, dens_union_le, subset_union_right, div_union, Turing.PartrecToTM2.contSupp_cons₁, union_smul_inter_subset_union, Nat.mul_divisors_filter_prime_pow, union_inter_distrib_right, Multiset.card_Ioo, DFinsupp.card_Icc, union_subset_iff, uIcc_subset_uIcc_union_uIcc, disjSups_union_right, powersetCard_succ_insert, mul_union, mulRothNumber_union_le, box_succ_union_prod, union_inter_cancel_right, symmDiff_eq_union, union_vadd, Set.Finite.toFinset_union, filter_union_filter_of_codisjoint, Nat.Coprime.primeFactors_mul, Finsupp.support_zipWith, addETransformRight_fst, sdiff_union_inter, prod_union_inter, mulETransformLeft_snd, sdiff_union_distrib, MeasureTheory.lmarginal_union', AhlswedeZhang.infSum_union_add_infSum_sups, union_union_distrib_left, List.toFinset_union, inf'_union, Nonempty.inr, infs_union_left, diffs_union_left, DFinsupp.card_Ioc, MvPolynomial.vars_add_of_disjoint, truncatedInf_union_right, mul_eq_mul_prime_prod, OrderEmbedding.birkhoffFinset_sup, card_truncatedSup_union_add_card_truncatedSup_infs, memberSubfamily_union, toRight_union, card_sdiff_add_card, DFinsupp.support_sup, union_div_inter_subset_union, Finsupp.support_sub, cast_card_inter, iSup_union, inter_add_union_subset, coe_union, SimpleGraph.isBipartiteWith_sum_degrees_eq_twice_card_edges, Turing.PartrecToTM2.codeSupp_comp
|