| Name | Category | Theorems |
|---|
coeEmb π | CompOp | 1 mathmath: coe_coeEmb
|
decidableDExistsFinset π | CompOp | β |
decidableDforallFinset π | CompOp | 6 mathmath: map_nsmul_piAntidiag, prod_ite_zero, Finpartition.mem_atomise, char_dvd_card_solutions_of_sum_lt, prod_boole, nsmul_piAntidiag
|
decidableEq π | CompOp | 45 mathmath: collapse_eq, IsLowerSet.le_card_inter_finset, Icc_eq_image_powerset, nonMemberSubfamily_union, memberSubfamily_image_erase, powerset_insert, inter_mem_infs, IsLowerSet.card_inter_le_finset, AhlswedeZhang.supSum_union_add_supSum_infs, powerset_sups_powerset_self, nonMemberSubfamily_inter, IsLowerSet.le_card_inter_finset', biUnion_slice, Finpartition.card_nonuniformWitnesses_le, powerset_infs_powerset_self, nonMemberSubfamily_image_insert, memberSubfamily_inter, DFinsupp.support_rangeIcc_subset, IsUpperSet.le_card_inter_finset, Ico_eq_image_ssubsets, powerset_image, union_mem_sups, memberSubfamily_image_insert, memberSubfamily_union_nonMemberSubfamily, Set.Sized.uvCompression, SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image, card_truncatedInf_union_add_card_truncatedInf_sups, slice_union_shadow_falling_succ, Finpartition.ofSetoid_parts_val, DFinsupp.card_pi, card_biUnion_le_of_intersecting, powerset_inter, card_le_card_biUnion_add_card_fiber, image_insert_memberSubfamily, shatters_iff, collapse_modular, sum_powerset_neg_one_pow_card, powerset_union, IsUpperSet.card_inter_le_finset, powersetCard_succ_insert, AhlswedeZhang.infSum_union_add_infSum_sups, four_functions_theorem, card_truncatedSup_union_add_card_truncatedSup_infs, memberSubfamily_union, Finpartition.ofSetSetoid_parts
|
decidableEqPiFinset π | CompOp | 1 mathmath: pi_insert
|
decidableExistsAndFinset π | CompOp | 5 mathmath: prod_ite_one, expect_ite_zero, Fintype.all_card_le_filter_rel_iff_exists_injective, sum_ite_zero, piFinset_filter_const
|
decidableExistsAndFinsetCoe π | CompOp | β |
decidableMem π | CompOp | 117 mathmath: MultilinearMap.map_piecewise_smul, expect_ite_mem, ContinuousMultilinearMap.map_piecewise_smul, UV.compress_injOn, collapse_eq, sum_ite_mem, sum_boole_mul, disjiUnion_filter_eq, MvPolynomial.coeff_X_mul', univ_pi_univ, FormalMultilinearSeries.changeOriginSeriesTerm_apply, Finsupp.if_mem_support, Nat.prod_mem_factoredNumbers, sum_card_fiberwise_eq_card_filter, sum_ite_eq', Fintype.card_filter_piFinset_eq, Fintype.prod_extend_by_one, Fintype.piFinset_update_eq_filter_piFinset_mem, MultilinearMap.map_piecewise_sub_map_piecewise, sdiff_eq_filter, card_erase_eq_ite, Profinite.NobelingProof.fin_comap_jointlySurjective, Finsupp.sum_ite_eq, Profinite.NobelingProof.GoodProducts.spanFin, sum_piecewise, prod_pi_mulSingle, prod_pi_mulSingle', Finsupp.sum_ite_eq', ContinuousAlternatingMap.map_piecewise_smul, Finsupp.indicator_apply, filter_univ_mem, prod_ite_eq', MultilinearMap.curryFinFinset_symm_apply_piecewise_const, ContinuousMultilinearMap.map_piecewise_add, update_eq_piecewise, Fintype.prod_ite_mem, Fintype.sum_ite_mem, sum_fiberwise_eq_sum_filter, ContinuousMultilinearMap.map_add_univ, Int.sum_modEq_ite, prod_eq_ite, MultilinearMap.map_add_sub_map_add_sub_linearDeriv, Profinite.NobelingProof.factors_prod_eq_basis_of_ne, prod_pow_boole, ContinuousMultilinearMap.curryFinFinset_apply_const, filter_eq', sum_dite_eq', SkewMonoidAlgebra.sum_ite_eq', prod_dite_eq, MultilinearMap.curryFinFinset_apply_const, expect_dite_eq', card_sq_le_card_mul_mulEnergy, Fintype.expect_ite_mem, MvPolynomial.coeff_mul_X', MultilinearMap.map_add_eq_map_add_linearDeriv_add, ContinuousAlternatingMap.map_add_univ, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const, MultilinearMap.map_piecewise_add, sum_boole_nsmul, card_sq_le_card_mul_addEnergy, prod_extend_by_one, Profinite.NobelingProof.spanFinBasis.span, card_insert_eq_ite, sum_extend_by_zero, inter_singleton, prod_ite_mem, Nat.prod_modEq_ite, piecewise_singleton, sum_pi_single', prod_fiberwise_eq_prod_filter', sum_pi_single, Equiv.Perm.ofSubtype_eq_iff, prod_ite_eq, sigma_preimage_mk, exists_finset_piecewise_mem_of_mem_nhds, Finsupp.prod_ite_eq, piecewise_erase_univ, inter_insert, image_insert_memberSubfamily, ContinuousAlternatingMap.map_piecewise_add, Function.updateFinset_def, Nat.sum_modEq_ite, DFinsupp.mk_apply, Affine.Simplex.ExcenterExists.signedInfDist_excenter, expect_dite_eq, PMF.uniformOfFinset_apply, UV.compress_disjoint, singleton_inter, Fintype.card_filter_piFinset_const, Equiv.Perm.IsCycle.forall_commute_iff, prod_dite_eq', Equiv.Perm.IsCycle.commute_iff, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, Fintype.sum_extend_by_zero, Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, sum_fiberwise_eq_sum_filter', filter_attach', MultilinearMap.map_sub_map_piecewise, Int.prod_modEq_ite, sum_dite_eq, FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm, expect_ite_eq, prod_piecewise, sum_mul_boole, Finsupp.prod_ite_eq', sum_ite_eq, Equiv.Perm.OnCycleFactors.kerParam_apply, expect_ite_eq', sum_eq_ite, Profinite.NobelingProof.factors_prod_eq_basis, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, prod_fiberwise_eq_prod_filter, filter_eq, Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff, MultilinearMap.map_add_univ, insert_inter
|
decidableMem' π | CompOp | 5 mathmath: SimpleGraph.neighborFinset_subset_between_union, SimpleGraph.neighborFinset_subset_between_union_compl, SimpleGraph.degree_le_between_add, SimpleGraph.degree_le_between_add_compl, schnirelmannDensity_finset
|
instDecidableLE π | CompOp | 5 mathmath: Set.Sized.uvCompression, card_truncatedInf_union_add_card_truncatedInf_sups, UV.card_compress, UV.toColex_compress_lt_toColex, card_truncatedSup_union_add_card_truncatedSup_infs
|
instDecidableLT π | CompOp | β |
instDecidableRelSSubset π | CompOp | 2 mathmath: Ioo_eq_filter_ssubsets, Ioc_eq_filter_powerset
|
instDecidableRelSubset π | CompOp | 7 mathmath: Finpartition.equitabilise_aux, Finpartition.card_parts_equitabilise_subset_le, Ico_eq_filter_ssubsets, Finpartition.card_filter_atomise_le_two_pow, filter_subset_univ, Finpartition.biUnion_filter_atomise, Icc_eq_filter_powerset
|
instHasSSubset π | CompOp | 59 mathmath: compl_ssubset_compl, exists_of_one_lt_card_pi, empty_ssubset, Iio_ssubset_Iio, val_lt_iff, Set.Finite.ssubset_toFinset, Set.toFinset_ssubset_toFinset, ssubset_singleton_iff, ssubset_iff_subset_ne, Ioo_eq_filter_ssubsets, Ioi_ssubset_Ioi, lt_eq_subset, ssubset_iff_exists_subset_erase, instIrreflSSubset, isWellFounded_ssubset, instAsymmSSubset, instIsNonstrictStrictOrderSubsetSSubset, instIsTransSSubset, map_ssubset_map, Icc_ssubset_Icc_left, not_ssubset_empty, Set.Finite.toFinset_ssubset_toFinset, ssubset_def, coe_ssubset, erase_ssubset_insert, Set.Finite.toFinset_ssubset, mem_ssubsets, Iic_ssubset_Iic, Icc_ssubset_Icc_right, SimpleGraph.edgeFinset_strict_mono, Set.toFinset_strict_mono, ssubset_iff, ssubset_univ_iff, Set.toFinset_ssubset, ssubset_iff_exists_cons_subset, Nonempty.empty_ssubset, Set.ssubset_toFinset, filter_ssubset, Ici_ssubset_Ici, attachFin_ssubset_attachFin_iff, YoungDiagram.cells_ssubset_iff, ssubset_insert, empty_ssubset_singleton, image_subtype_univ_ssubset_image_univ, sdiff_ssubset, Ioc_eq_filter_powerset, Set.toFinset_ssubset_univ, Multiset.toFinset_ssubset, Geometry.SimplicialComplex.not_facet_iff_subface, pow_ssubset_pow_succ_of_pow_ne_closure, Set.Finite.toFinset_strictMono, lt_iff_ssubset, erase_ssubset, PairReduction.finset_logSizeBallSeq_add_one_ssubset, nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure, image_ssubset_image, ssubset_cons, ssubset_iff_of_subset, SimpleGraph.edgeFinset_ssubset_edgeFinset
|
instHasSubset π | CompOp | 629 mathmath: Polynomial.supp_subset_range, SimpleGraph.edgeFinset_mono, WittVector.remainder_vars, disjSups_subset_iff, DFinsupp.support_zipWith, Finsupp.support_finset_sum, MvPolynomial.support_sum, Nonempty.subset_one_iff, mul_inter_subset, MvPolynomial.support_mul, image_subset_infs_left, smulAntidiagonal_mono_right, rothNumberNat_spec, DFinsupp.support_mono, Nat.smoothNumbersUpTo_subset_image, smul_finset_subset_smul_finset_iff, Ico_subset_Ico_right, mul_subset_iff_right, addETransformRight.fst_add_snd_subset, YoungDiagram.cells_subset_iff, SimpleGraph.cliqueFinset_mono, MonoidAlgebra.support_one_subset, SimpleGraph.edgeFinset_subset_sym2_of_support_subset, toLeft_eq_univ, MeasureTheory.SimpleFunc.range_comp_subset_range, image_subset_diffs_right, Finpartition.nonUniforms_mono, Ico_subset_Ico_union_Ico, subset_product_image_snd, subset_mul, inter_subset_ite, vaddAntidiagonal_mono_left, Finpartition.equitabilise_aux, mem_upShadow_iff_exists_mem_card_add, Icc_subset_Iic_self, Set.subset_toFinset, slice_subset, inter_sub_union_subset_union, UV.shadow_compression_subset_compression_shadow, Turing.PartrecToTM2.trStmtsβ_trans, sdiff_nonempty, subset_add_right, Turing.PartrecToTM2.codeSupp_self, subset_nsmul, Finpartition.parts_subset_extendOfLE, Finpartition.card_parts_equitabilise_subset_le, inter_eq_inter_iff_left, mem_shadow_iterate_iff_exists_sdiff, Nat.filter_range_nth_subset_insert, Ioo_subset_Ici_self, smul_finset_subset_smul, inter_subset_right, subset_empty, Int.erdos_ginzburg_ziv, mem_finsuppAntidiag, ite_subset_union, cons_subset_cons, falling_zero_subset, disjSum_subset, subset_smul_finset_iff, slice_subset_falling, pow_subset_pow_right, op_smul_finset_subset_mul, add_mul_subset, SkewMonoidAlgebra.support_one_subset, noncommSum_union_of_disjoint, instIsTransSubset, Finsupp.support_mul, attachFin_ssubset_attachFin, biUnion_subset_iff_forall_subset, imageβ_subset_iff_right, MvPolynomial.support_sdiff_support_subset_support_add, div_zero_subset, Finsupp.eq_single_iff, exists_subset_or_subset_of_two_mul_lt_card, Ioc_subset_Iic_self, Icc_subset_uIcc', IsPrimitiveRoot.is_roots_of_minpoly, sups_inter_subset_right, SkewMonoidAlgebra.support_sum, Subset.rfl, Nat.divisors_subset_of_dvd, subset_sups, ruzsa_covering_add, addDysonETransform.subset, Nat.primeFactors_subset_of_mem_smoothNumbers, Finsupp.mapDomain_support, Polynomial.support_C_mul_X', smul_finset_subset_smul_finset_iffβ, Multiset.support_sum_subset, Ioo_subset_Icc_self, ruzsa_covering_mul, ssubset_iff_subset_ne, subset_insert_iff_of_notMem, map_symm_subset, support_sum_subset, subset_map_inl, subset_of_le, Subset.refl, image_subset_image_iff, MvPolynomial.coeffs_one, inter_vadd_subset, SimpleGraph.extend_finset_to_connected, insert_subset_iff, ssubset_iff_exists_subset_erase, Polynomial.support_trinomial', union_eq_left, subset_add, inter_sub_subset, Icc_subset_Ioc_iff, wittStructureRat_vars, Icc_subset_Icc_left, DFinsupp.support_mk_subset, noncommProd_union_of_disjoint, Turing.TM1.stmtsβ_trans, Ici_mul_Ioi_subset', Set.Finite.toFinset_subset, subset_div_left, PartitionOfUnity.eventually_fintsupport_subset, vadd_subset_iff, Colex.IsInitSeg.total, MvPolynomial.support_add, mulRothNumber_spec, sups_infs_subset_left, instReflSubset, mem_subsetSum_iff, imageβ_subset_iff, union_vadd_inter_subset_union, vadd_inter_subset, Icc_subset_Ico_iff, exists_subset_of_mem_upShadow, image_subset_sups_left, infs_sups_subset_right, card_le_one_iff_subset_singleton, Ico_subset_Ico_left, Nat.primeFactors_mono, subset_div, subset_mul_right, AddMonoidAlgebra.support_mul_single_subset, univ_subset_iff, Set.Sized.subset_powersetCard_univ, one_subset, uIcc_subset_uIcc_right, imageβ_inter_union_subset, Iic_add_Iic_subset, op_vadd_finset_subset_add, mem_finsupp_iff, uIcc_subset_uIcc, Polynomial.support_binomial', Finpartition.parts_top_subset, SimpleGraph.neighborFinset_subset_between_union, subset_addSpan, inter_eq_inter_iff_right, Shatters.subset_iff, MvPolynomial.support_expand_subset, subset_add_left, Subset.antisymm_iff, instIsNonstrictStrictOrderSubsetSSubset, Ico_eq_filter_ssubsets, AddMonoidAlgebra.support_single_mul_subset, vsub_subset_iff, Finsupp.support_mul_subset_right, addAntidiagonal_mono_right, compls_subset_iff, filter_subset, MvPolynomial.vars_sub_subset, subset_compl_singleton, vadd_finset_subset_iff, subset_range_sup_succ, uIcc_subset_uIcc_iff_le', inter_vsub_subset, smul_finset_inter_subset, uIcc_subset_uIcc_iff_le, exists_subset_card_eq, WittVector.wittZSMul_vars, exists_subset_of_mem_shadow, Ici_mul_Ici_subset', Ici_add_Ioi_subset, Finsupp.frange_single, SimpleGraph.neighborFinset_subset_between_union_compl, DFinsupp.subset_support_tsub, smulAntidiagonal_mono_left, singleton_subset_iff, Finpartition.mem_atomise, shatterer_compress_subset_shatterer, image_subset_sups_right, image_subset_diffs_left, DFinsupp.support_tsub, smul_finset_subset_iffβ, subset_powersetCard_univ_iff, Icc_subset_Ico_right, subset_diffs, sym_union, subset_cons, monotone_filter_right, add_inter_subset, SimpleGraph.incidenceFinset_subset, range_subset, SimpleGraph.isBipartiteWith_neighborFinset_subset, add_subset_iff_right, right_eq_union, DFinsupp.support_rangeIcc_subset, Finsupp.support_sum, addRothNumber_spec, range_subset_range, SkewPolynomial.support_add, SimpleGraph.right_nonuniformWitnesses_subset, wittPolynomial_vars_subset, subset_union_left, disjSups_inter_subset_right, DFinsupp.support_mk'_subset, exists_superset_card_eq, Finsupp.support_subset_singleton, singleton_subset_coe, Iic_mul_Iic_subset', SzemerediRegularity.biUnion_star_subset_nonuniformWitness, Polynomial.support_C_subset, SzemerediRegularity.star_subset_chunk, Icc_subset_Ici_self, Multiset.toEnumFinset_mono, Polynomial.support_C_mul_X_pow', ssubset_def, inter_subset_union, Nat.properDivisors_subset_divisors, mem_upShadow_iterate_iff_exists_card, Finsupp.support_ceilDiv_subset, pimage_inter, Turing.PartrecToTM2.codeSupp'_self, compls_subset_compls, add_subset_iff, PartitionOfUnity.eventually_finsupport_subset, Finsupp.support_sym2Mul_subset, Polynomial.supp_subset_range_natDegree_succ, symmDiff_subset_sdiff, WittVector.mul_polyOfInterest_vars, Polynomial.roots_expand_image_frobenius_subset, erase_insert_subset, piDiag_subset_piFinset, Ico_add_Icc_subset, Multiset.toEnumFinset_subset_iff, vadd_finset_subsetSum_subset_subsetSum_insert, Polynomial.support_add, addETransformLeft.fst_add_snd_subset, symmDiff_subset_union, toLeft_eq_empty, inter_smul_union_subset_union, SimpleGraph.not_isUniform_iff, zero_subset, Ioc_subset_Ici_self, smul_finset_subset_iff, WittVector.wittAdd_vars, MonoidAlgebra.support_mul_single_subset, Ico_mul_Icc_subset', Ioc_mul_Ico_subset', Ioc_subset_Icc_self, mulDysonETransform.subset, Behrend.sphere_zero_subset, mem_powerset, covBy_iff_card_sdiff_eq_one, image_subset_iff_subset_preimage, imageβ_union_inter_subset_union, UniqueFactorizationMonoid.radical_dvd_radical_iff_primeFactors_subset_primeFactors, Icc_subset_Icc_iff, mem_powersetCard, Set.Finite.toFinset_mono, image_subset_Iic_sup, mapRange_finsuppAntidiag_subset, toRight_eq_univ, SkewMonoidAlgebra.support_add, add_subset_iff_left, SimpleGraph.unreduced_edges_subset, EMetric.pair_reduction, Set.toFinset_subset, pimage_subset, subset_def, subset_product_image_fst, instAntisymmSubset, Preorder.frestrictLeβ_apply, Finsupp.support_mapRange, Set.Finite.subset_toFinset, subset_one_iff_eq, MvPolynomial.vars_prod, zero_div_subset, diffs_inter_subset_left, AddMonoidAlgebra.support_mul, Finpartition.sparsePairs_mono, mulDysonETransform.smul_finset_snd_subset_fst, imageβ_inter_union_subset_union, Nontrivial.not_subset_singleton, Finsupp.support_mono, ssubset_iff, wittStructureInt_vars, le_card_iff_exists_subset_card, Finpartition.part_subset, Iio_subset_Iic_self, nsmul_subset_nsmul_right, erase_image_subset_image_erase, Icc_subset_Icc, Iic_mul_Iio_subset', SmoothPartitionOfUnity.eventually_fintsupport_subset, Ico_subset_Iic_self, sups_infs_subset_right, image_subset_iff, Ioc_subset_Ioi_self, xInTermsOfW_vars_subset, Polynomial.support_integralNormalization_subset, sups_subset_self, AddMonoidAlgebra.support_one_subset, imageβ_distrib_subset_right, MulAction.mem_stabilizer_finset_iff_smul_finset_subset, Iic_subset_Iic, uIcc_subset_uIcc_left, Set.Finite.toFinset_subset_toFinset, imageβ_inter_subset_right, image_subset_imageβ_left, Fintype.eval_image_piFinset_subset, Polynomial.support_smul, mul_subset_iff_left, div_subset_iff, SkewMonoidAlgebra.support_mul_single_subset, Ico_subset_Ico_iff, image_inter_subset, Finsupp.support_single_add_single_subset, Nat.mem_factoredNumbers_iff_primeFactors_subset, Finsupp.support_floorDiv_subset, mulAntidiagonal_mono_left, Infinite.exists_superset_card_eq, subset_iff_eq_of_card_le, uIcc_subset_uIcc_iff_mem, SkewMonoidAlgebra.support_mul, subset_biUnion_of_mem, subset_mulSpan, ssubset_iff_exists_cons_subset, union_eq_right, map_inl_subset_iff_subset_toLeft, imageβ_distrib_subset_left, mul_add_subset, Polynomial.coeffs_one, subset_sdiff, sub_inter_subset, subset_vadd, MvPolynomial.support_monomial_subset, Icc_subset_uIcc, WittVector.wittSub_vars, image_subset_infs_right, sdiff_eq_empty_iff_subset, union_mul_inter_subset, Iio_mul_Iic_subset', inter_mul_union_subset, Icc_mul_Ico_subset', inter_mul_union_subset_union, IsLowerSet.memberSubfamily_subset_nonMemberSubfamily, Nat.primeFactors_subset_of_mem_factoredNumbers, left_eq_union, Turing.TM2.stmtsβ_trans, Ioo_subset_Ioo_right, subset_map_iff, Finsupp.subset_support_tsub, SkewMonoidAlgebra.support_single_subset, mem_falling, subset_sub_left, Finpartition.card_filter_atomise_le_two_pow, AddMonoidAlgebra.mem_grade_iff, WittVector.wittPow_vars, subset_univ_image_iff, Nat.divisors_subset_properDivisors, subset_iff, uIcc_subset_Icc, Finsupp.support_smul, Ideal.decomposition_erase_inf, Finsupp.support_update_subset, Ico_add_Ioc_subset, subset_subsetSum, subset_sub, prod_powerset_cons, SmoothPartitionOfUnity.finsupport_subset_fintsupport, Ioi_subset_Ioi, imageβ_inter_subset_left, map_inr_subset_iff_subset_toRight, vadd_finset_subset_add, imageβ_union_inter_subset, toRight_eq_empty, Ioo_subset_Ioc_self, Ioo_subset_Ioo_left, inter_pow_subset, MvPolynomial.vars_bindβ, Icc_subset_Ioo_iff, inter_smul_subset, exists_subset_mulSpan_card_le_of_forall_mulDissociated, inter_div_union_subset_union, MvPolynomial.vars_mul, mem_shadow_iff_exists_sdiff, filter_subset_univ, Iio_add_Iic_subset, mulAntidiagonal_mono_right, subset_compl_comm, imageβ_subset_iff_left, subset_zero_iff_eq, symmDiff_subset_sdiff', MvPolynomial.vars_pow, le_eq_subset, AddAction.mem_stabilizer_finset_iff_subset_vadd_finset, Icc_mul_Icc_subset', List.support_sum_subset, Ico_subset_Iio_self, PartitionOfUnity.finsupport_subset_fintsupport, Iic_add_Iio_subset, Ioi_add_Ici_subset, DirectSum.support_of_subset, mem_upShadow_iff_exists_sdiff, neg_subset_sub_right, inter_eq_right, vadd_finset_inter_subset, Polynomial.support_map_subset, MvPolynomial.support_map_subset, inter_nsmul_subset, Finsupp.support_add, MultilinearMap.support_dfinsuppFamily_subset, union_eq_union_iff_right, WittVector.polyOfInterest_vars, subset_set_imageβ, Finsupp.support_onFinset_subset, Shatters.exists_superset, Ici_add_Ici_subset, Finsupp.support_subset_singleton', MvPolynomial.coeffs_map, Geometry.SimplicialComplex.face_subset_face_iff, erase_subset_iff_of_mem, subset_insert, subset_singleton_iff, FreeAbelianGroup.support_add, Ico_subset_Icc_self, SimpleGraph.edgeFinset_subset_edgeFinset, sub_subset_iff, subset_singleton_iff', DFinsupp.support_single_subset, union_add_inter_subset, Ioc_subset_Ioc, mul_subset_iff, inter_eq_left, Nat.mem_smoothNumbers_iff_primeFactors_subset, Finsupp.cons_support, Set.toFinset_subset_toFinset, SkewMonoidAlgebra.support_single_mul_subset, SimpleGraph.left_nonuniformWitnesses_subset, Ioo_subset_Iic_self, Multiset.toFinset_subset, Ioi_subset_Ici_self, PairReduction.finset_logSizeBallSeq_add_one_subset, DFinsupp.support_add, attachFin_subset_attachFin_iff, PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init, addDysonETransform.vadd_finset_snd_subset_fst, subset_erase, support_subset_support_matPolyEquiv, singleton_subset_singleton, biUnion_subset, Nonempty.subset_zero_iff, Iio_subset_Iio, sups_subset_iff, MvPolynomial.vars_map, MvPolynomial.support_sub, xInTermsOfW_vars_aux, mulETransformRight.fst_mul_snd_subset, DirectSum.support_smul, Ioc_subset_Ioo_right, image_subset_imageβ_right, MvPolynomial.vars_rename, UniqueFactorizationMonoid.radical_dvd_iff_primeFactors_subset, mem_upShadow_iff_exists_mem_card_add_one, subset_sups_self, union_eq_union_iff_left, Icc_add_Icc_subset, subset_map_symm, Polynomial.support_derivativeFinsupp_subset_range, Numbering.IsPrefix.subset_of_card_le_card, subset_map_inr, Polynomial.roots_expand_pow_image_iterateFrobenius_subset, not_subset, map_subset_iff_subset_preimage, Finsupp.support_mul_subset_left, Finsupp.support_single_subset, div_inter_subset, subset_image_iff, union_mul_inter_subset_union, diffs_subset_iff, Ioc_add_Ico_subset, empty_subset, vadd_finset_subset_vadd, IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic, subset_inter_iff, WittVector.wittNSMul_vars, Icc_add_Ico_subset, exists_eq_insert_iff, MeasureTheory.SimpleFunc.range_const_subset, Nonempty.subset_singleton_iff, subset_smul_finset_iffβ, union_add_inter_subset_union, SmoothPartitionOfUnity.eventually_finsupport_subset, Ioo_subset_Ico_self, union_sub_inter_subset_union, powerset_mono, vaddAntidiagonal_mono_right, inter_add_union_subset_union, smul_inter_subset, subset_vsub, LaurentPolynomial.support_C_mul_T, subset_product, inter_vadd_union_subset_union, Ico_subset_Ioo_left, Ioo_subset_Iio_self, subset_disjSum, subset_smul, mem_shadow_iterate_iff_exists_mem_card_add, Set.toFinset_subset_toFinset_of_subset, subset_of_eq, Ioc_subset_Ioc_right, Ioo_subset_Ioi_self, disjSups_subset_sups, subset_Iic_sup_id, le_iff_subset, MvPolynomial.coeffs_C_subset, infs_sups_subset_left, Ico_subset_Ici_self, range_pow_padicValNat_subset_divisors', infs_self_subset, exists_subset_addSpan_card_le_of_forall_addDissociated, subset_shatterer, ZMod.erdos_ginzburg_ziv, vadd_finset_subset_vadd_finset_iff, map_subset_map, Polynomial.support_monomial', subset_vadd_finset_iff, Ioo_subset_Ioo, sum_powerset_cons, insert_subset_insert_iff, smul_subset_iff, subset_mul_left, mem_shadow_iff_exists_mem_card_add_one, mem_finsuppAntidiag', MvPolynomial.vars_add_subset, sups_inter_subset_left, Ico_mul_Ioc_subset', zero_smul_finset_subset, MvPolynomial.support_symmDiff_support_subset_support_add, PairReduction.pairSet_subset, Set.toFinset_mono, subset_compl_iff_disjoint_left, subset_pow, MonoidAlgebra.support_single_mul_subset, zero_smul_subset, infs_inter_subset_left, zero_mul_subset, insert_erase_subset, Finsupp.support_tsub, not_linearIndepOn_finset_iffββ, subset_union_right, smul_zero_subset, inv_subset_div_right, SimpleGraph.isBipartiteWith_neighborFinset_subset', HahnSeries.SummableFamily.support_powerSeriesFamily_subset, SimpleGraph.nonuniformWitness_subset, union_smul_inter_subset_union, mul_zero_subset, isDirected_subset, Submodule.decomposition_erase_inf, DFinsupp.support_sum, sdiff_subset, union_subset_iff, uIcc_subset_uIcc_union_uIcc, inter_div_subset, MonoidAlgebra.support_mul, DFinsupp.support_mapRange, inter_subset_left, WittVector.wittNeg_vars, MvPolynomial.support_smul, inter_add_subset, infs_subset_iff, subset_infs, mem_upShadow_iterate_iff_exists_sdiff, mem_dfinsupp_iff, infs_inter_subset_right, Finsupp.support_zipWith, compl_subset_compl, Behrend.sphere_subset_box, Ici_subset_Ici, Finsupp.subset_mapRange_neLocus, Icc_eq_filter_powerset, range_pow_padicValNat_subset_divisors, MvPolynomial.vars_sum_subset, val_le_iff, diffs_inter_subset_right, WittVector.wittPolyProd_vars, cons_subset, erase_subset, Set.Intersecting.exists_card_eq, disjSups_inter_subset_left, subset_univ, exists_cycleOn, DFinsupp.support_smul, addAntidiagonal_mono_left, subset_range, coe_subset_singleton, Set.Sized.isAntichain, Icc_subset_Icc_right, subset_infs_self, Finpartition.exists_subset_part_bijOn, MulAction.mem_stabilizer_finset_iff_subset_smul_finset, subset_compl_iff_disjoint_right, exists_nat_subset_range, WittVector.wittPolyProdRemainder_vars, Ioi_mul_Ici_subset', inter_mul_subset, mulETransformLeft.fst_mul_snd_subset, union_div_inter_subset_union, subset_insert_iff, Finsupp.support_sub, Ioc_subset_Ioc_left, AddAction.mem_stabilizer_finset_iff_vadd_finset_subset, Finpartition.subset, inter_add_union_subset, vsub_inter_subset, WittVector.wittMul_vars, DFinsupp.subset_mapRange_neLocus, Ico_subset_Ico, smul_finset_subset_mul, Set.powersetCard.eq_iff_subset, coe_subset, mem_upShadow_iterate_iff_exists_mem_card_add
|
instMembership π | CompOp | 1316 mathmath: Finpartition.mem_part_ofSetSetoid_iff_rel, List.mem_toFinset, iSup_biUnion, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff', expect_ite_mem, LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset, UV.compress_injOn, RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero, disjSups_subset_iff, notMem_singleton, Colex.mem_initSeg_self, Nonempty.zero_mem_sub, set_biInter_finset_image, filter_notMem_eq_sdiff, Nat.mem_properDivisors_prime_pow, notMem_Ioi_self, ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter, right_notMem_Ioo, Set.powersetCard.exist_mem_powersetCard_of_inf, Finsupp.sum_indicator_index_eq_sum_attach, Summable.sum_add_tsum_subtype_compl, pimage_eq_image_filter, Submodule.exists_finset_of_mem_iSup, Finsupp.mem_support_iff, zero_mem_sub_iff, Int.mem_divisorsAntidiag, Fintype.mem_piFinset, Equiv.Perm.mem_toList_iff, exists_card_fiber_lt_of_card_lt_nsmul, mem_pow, mem_zpowers_iff_mem_range_orderOf, mem_univ, Filter.frequently_exists_finset, MvPolynomial.exists_finset_rename, Metric.AreSeparated.finset_iUnion_right_iff, exists_mem_eq_inf, finite_cover_nhds, sum_ite_mem, set_biUnion_biUnion, disjUnion_singleton, zero_mem_subsetSum, mk_mem_sym2_iff, inv_smul_mem_iff, WithBot.sum_eq_bot_iff, Equiv.Perm.mem_cycleFactorsFinset_conj, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, closure_biUnion, MvPolynomial.mem_image_support_coeff_finSuccEquiv, sum_boole_mul, mem_sumLiftβ, disjiUnion_filter_eq, SetTheory.PGame.Domineering.mem_right, Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt, SupIndep.attach, le_fold_max, mem_singleton, MvPolynomial.coeff_X_mul', Set.biUnion_finsetSigma, YoungDiagram.mem_row_iff, mem_dfinsupp_iff_of_support_subset, eq_univ_iff_forall, mem_range_iff_mem_finset_range_of_mod_eq, ProbabilityTheory.Kernel.iIndep.meas_biInter, univ_pi_univ, Fin.attachFin_Iic, indicator_biUnion, attach_eq_univ, mem_image_const, InfPrime.finset_inf_le, left_mem_Icc, mem_upShadow_iff_exists_mem_card_add, forall_mem_not_eq, PairReduction.point_notMem_finset_logSizeBallSeq_add_one, le_sup'_iff, exists_ne_zero_of_sum_ne_zero, Nat.swap_mem_divisorsAntidiagonal, singleton_disjUnion, Nat.mem_factoredNumbers', ProbabilityTheory.iIndepFun_iff, fold_min_lt, ProbabilityTheory.iIndep.meas_biInter, mem_singleton_self, sigma_nonempty, Nat.mem_finMulAntidiag, YoungDiagram.mem_cells, mk_mem_sigmaLift, left_notMem_Ioo, MeasureTheory.Measure.ae_mem_finset_iff, Filter.mem_iInf_finite, MeasureTheory.lintegral_biUnion_finsetβ, IsPrimitiveRoot.mem_nthRootsFinset, Finsupp.if_mem_support, MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal, ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul, Nat.one_mem_properDivisors_iff_one_lt, IsSemilinearSet.biUnion_finset, LocallyFiniteOrder.finset_mem_Icc, Equiv.Perm.notMem_support, inf_lt_iff, MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen, mem_sym_iff, SimpleGraph.TripartiteFromTriangles.rel_iff, Nonempty.exists_mem, SimpleGraph.IsNClique.exists_not_adj_of_cliqueFree_succ, SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq, set_encard_biUnion_le, convolution_ne_zero, mem_shadow_iterate_iff_exists_sdiff, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, Nat.prod_mem_factoredNumbers, Set.finite_mem_finset, sum_card_fiberwise_eq_card_filter, Fin.mem_piFinset_iff_pivot_removeNth, ProbabilityTheory.iIndepFun.measure_inter_preimage_eq_mul, MvPolynomial.mem_support_iff, BoxIntegral.unitPartition.mem_prepartition_boxes_iff, Ideal.IsPrime.prod_le, Fin.attachFin_Ioo_eq_Ioi, MvPolynomial.notMem_support_iff, coe_filter, BoxIntegral.unitPartition.mem_admissibleIndex_iff, Set.Infinite.exists_notMem_finset, Nonempty.sup_eq_top_iff, DFinsupp.mem_neLocus, right_mem_Ioc, inf'_lt_iff, isIrreducible_iff_sUnion_isClosed, one_mem_one, prod_ite_one, Rel.mk_mem_interedges_comm, attach_nonempty_iff, DFinsupp.prod_eq_zero_iff, Colex.toColex_lt_toColex_iff_max'_mem, Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, set_biUnion_coe, MeasureTheory.lintegral_biUnion_finset, lt_sup'_iff, mem_insert_self, mem_finsuppAntidiag, setOf_liouvilleWith_subset_aux, mem_sup, UpperHalfPlane.prod_eq_zero_iff, LieModule.genWeightSpaceChain_def', MeasureTheory.Measure.ae_mem_finset_iff_map_eq_sum_dirac, mem_mk, nullMeasurableSet_biUnion, Equiv.Perm.Basis.mem_support_self', mem_uIcc', SimpleGraph.regularityReduced_adj, isLindelof_biUnion, MeasureTheory.Measure.haar.index_elim, mem_Ici, biUnion_range_succ_disjointed, Filter.iInf_principal_finset, SummationFilter.eventually_mem_or_not_mem, inf_le_iff, set_biUnion_finset_image, mem_sum, sum_ite_eq', HallMarriageTheorem.hall_hard_inductive, Colex.le_iff_max'_mem, indicator_biUnion_apply, IsSemilinearSet.biInter_finset, IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo, one_mem_div_iff, Equiv.Perm.mem_support_iff_of_commute, finprod_mem_finset_product, ProbabilityTheory.Kernel.map_partialTraj_succ_self, UniqueMul.exists_iff_exists_existsUnique, mem_image_univ_iff_mem_range, swap_mem_mulAntidiagonal, inr_mem_sumLexLift, DFinsupp.mem_support_toFun, mem_generatePiSystem_iUnion_elim, Fintype.card_filter_piFinset_eq, Ioc_subset_biUnion_Ioc, Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag, addConvolution_eq_zero, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff, Fintype.prod_extend_by_one, biUnion_nonempty, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff', mem_image, Nat.mem_properDivisors_iff_exists, Finpartition.mk_mem_nonUniforms, IsNonarchimedean.finset_image_add, summable_compl_iff, Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff', eventuallyEq_iInter, Fintype.piFinset_update_eq_filter_piFinset_mem, Equiv.Perm.IsThreeCycle.support_eq_iff_mem_support, Colex.lt_iff_exists_forall_lt, CovBy.exists_finset_erase, MultilinearMap.map_piecewise_sub_map_piecewise, Polynomial.natDegree_notMem_eraseLead_support, Equiv.Perm.SameCycle.mem_support_iff, Algebra.EssFiniteType.adjoin_mem_finset, IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf, Set.biUnion_finsetSigma_univ, coe_bipartiteBelow, expect_ite_zero, Algebra.adjoin_attach_biUnion, Equiv.Perm.IsCycle.commute_iff', Ideal.subset_union_prime', mem_mulAntidiagonal, Fin.insertNth_mem_piFinset_insertNth, Finsupp.notMem_support_iff, indicator_biUnion_finset_eventuallyEq, iInf_eq_iInf_finset', MonomialOrder.degree_mem_support_iff, sdiff_eq_filter, ENNReal.tsum_biUnion_le, FinsetCoe.canLift, mem_sort, Prime.exists_mem_finset_dvd, ExpGrowth.expGrowthSup_sum, ConcaveOn.exists_le_of_centerMass, DFinsupp.notMem_support_iff, zero_mem_smul_finset_iff, Submodule.fg_biSup, IsLocalization.coeffIntegerNormalization_mem_support, LocallyFinite.exists_finset_nhds_support_subset, MeasureTheory.SimpleFunc.mem_range, erase_injOn', MvPolynomial.mem_vars, Polynomial.mem_support_derivative, frequently_exists, MeasureTheory.integrableOn_finset_iUnion, LinearMap.iInf_ker_proj_le_iSup_range_single, Filter.iInf_sets_eq_finite', filter_nonempty_iff, sum_attach_eq_sum_dite, IntermediateField.finiteDimensional_iSup_of_finset, Colex.mem_initSeg, MeasureTheory.FiniteMeasure.restrict_biUnion_finset, attach_eq_empty_iff, exists_ne_map_eq_of_card_lt_of_maps_to, smul_mem_smul_finset_iff, restrictβ_preimage, Set.biInter_finsetSigma', mem_zero, Nat.mem_divisors, Finpartition.mem_avoid, insert_eq_self, card_erase_eq_ite, sup_set_eq_biUnion, ProbabilityTheory.Kernel.iIndepSet.meas_biInter, smul_mem_smul_finset_iffβ, FirstOrder.Ring.lift_genericPolyMap, sum_pos_iff, ProbabilityTheory.iCondIndep_iff, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, max'_mem, MeasureTheory.SimpleFunc.mem_range_of_measure_ne_zero, Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff, MeasureTheory.IsSetSemiring.disjointOfUnion_props, Set.Finite.mem_toFinset, attach_insert, mem_vadd, insert_subset_iff, ssubset_iff_exists_subset_erase, mem_uIcc_of_le, SimpleGraph.notMem_neighborFinset_self, prod_indicator_apply, nullMeasurableSet_biInter, iInf_insert, disjiUnion_disjiUnion, Profinite.NobelingProof.fin_comap_jointlySurjective, MeasureTheory.integral_biUnion_finset, UpperSemicontinuousOn.inter_biInter_preimage_Ici_eq_empty_iff_exists_finset, Colex.toColex_le_toColex_iff_max'_mem, exists_minimal, set_biInter_coe, Finsupp.sum_ite_eq, PairReduction.point_mem_logSizeBallSeq_init, mem_vaddAntidiagonal, Module.exists_nontrivial_relation_of_finrank_lt_card, Profinite.NobelingProof.GoodProducts.spanFin, Finsupp.mem_rangeSingleton_apply_iff, mem_filter_univ, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, Set.biInter_finsetSigma, Int.prodMk_mem_divisorsAntidiag, absorbs_biUnion_finset, eventuallyLE_iInter, iSup_coe, IsCompact.exists_finite_cover_smul, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff, inr_mem_disjSum, inf_sup, vadd_subset_iff, Equiv.Perm.mem_support, Set.biUnion_empty_finset, hasSum_sum_disjoint, iInf_coe, iSup_singleton, SupIrred.finset_sup_eq, biSup_finsetSigma', Set.iInter_eq_iInter_finset, SimpleGraph.mem_incidenceFinset, coe_mem, mul_mem_smul_finset_iff, PMF.mem_support_ofFinset_iff, Ideal.IsPrime.inf_le', mem_inv_smul_finset_iff, zero_mem_neg_add_iff, Colex.singleton_le_toColex, mem_subsetSum_iff, imageβ_subset_iff, mem_sub, ENNReal.tendsto_tsum_compl_atTop_zero, MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure, Fin.attachFin_Icc, AddMonoid.exponent_eq_max'_addOrderOf, mem_range_succ_iff, prod_pi_mulSingle, min'_mem, exists_le_of_prod_le', Equiv.Finset.union_inl, mem_Iic, subtype_eq_univ, ProbabilityTheory.iIndepFun.meas_biInter, DFinsupp.mem_singleton_apply_iff, Subgroup.leftCoset_cover_const_iff_surjOn, Equiv.Perm.mem_support_cycleOf_iff, Submodule.span_attach_biUnion, right_mem_uIcc, Set.biInter_finsetSigma_univ, Fin.attachFin_Ico_eq_Ici, TwoUniqueProds.uniqueMul_of_one_lt_card, ProbabilityTheory.iIndepSets_iff, wellFoundedOn_bUnion, prod_pi_mulSingle', MeasureTheory.SimpleFunc.preimage_eq_empty_iff, LocallyFiniteOrder.finset_mem_Ioo, exists_card_fiber_le_of_card_le_mul, Finsupp.sum_ite_eq', all_card_le_biUnion_card_iff_existsInjective', SimpleGraph.IsFiveWheelLike.snd_notMem, Nat.mem_divisorsAntidiagonal, Nat.mem_factoredNumbers_iff_forall_le, one_subset, Set.definable_finset_biInter, mem_insert_coe, PMF.mem_support_ofMultiset_iff, set_biUnion_singleton, BoxIntegral.Prepartition.mem_mk, Multiset.mem_sup_map_support_iff, PartitionOfUnity.exists_finset_nhds_support_subset, mem_finsupp_iff, Finsupp.indicator_apply, Ideal.iInf_sup_eq_top, InfIrred.finset_inf_eq, coe_bipartiteAbove, filter_univ_mem, MvPolynomial.zero_notMem_coeffs, ProbabilityTheory.Kernel.iIndepSets.meas_biInter, IsOfFinOrder.mem_powers_iff_mem_range_orderOf, Shatters.subset_iff, one_lt_card_iff, prod_ite_eq', mem_attach, Finpartition.part_eq_empty, LocallyFiniteOrderTop.finset_mem_Ici, IsUltrametricDist.exists_norm_finset_prod_le, Filter.mem_iInf_finite', eq_empty_iff_forall_notMem, IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty, UniqueProds.uniqueMul_of_nonempty, vsub_subset_iff, sum_erase_attach, Equiv.Perm.mem_support_iff_mem_support_of_mem_cycleFactorsFinset, attach_affineCombination_coe, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map, covBy_iff_exists_insert, isCompact_iff_finite_subcover, fiber_nonempty_iff_mem_image, exists_ne_map_eq_of_card_image_lt, IsCompact.exists_finite_cover_vadd, tendsto_mulIndicator_biUnion_finset, codisjoint_left, Equiv.Perm.mem_support_cycleOf_iff', MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, nonempty_def, MeasureTheory.IsSetRing.biInter_mem, exists_mem_imageβ, subset_compl_singleton, Subgroup.FG.biSup_finset, FreeMonoid.mem_symbols, mem_mulSpan, Besicovitch.exist_finset_disjoint_balls_large_measure, max_mem_image_coe, Finsupp.mem_neLocus, mem_Icc, exists_mem_insert, mem_one, exists_minimalFor, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_Ο_app_eq_sum, mem_diag, Nonempty.ciSup_mem_image, Fintype.prod_ite_mem, one_lt_prod_iff_of_one_le, BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box, MeasureTheory.measureReal_biUnion_finset, Set.powersetCard.mem_coe_iff, singleton_subset_iff, Finpartition.mem_atomise, sum_attach, SimpleGraph.mem_finsetWalkLength_iff, Nat.one_mem_divisors, MeasureTheory.IsSetAlgebra.biUnion_mem, one_mem_inv_mul_iff, IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf, Polynomial.mem_support_iff, setOf_mem, MeasureTheory.IsSetAlgebra.biInter_mem, Fintype.sum_ite_mem, iSup_eq_iSup_finset, FixedDetMatrices.reps_entries_le_m', SimpleGraph.mem_indepSetFinset_iff, mem_filterMap, mem_disjSups, sup_attach, Finsupp.prod_attach_index, exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul, mem_pimage, mem_sigmaLift, inl_mem_sumLiftβ, Polynomial.coeff_mem_coeffs, MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero, Set.PairwiseDisjoint.attach, mem_piDiag, exists_max_image, Set.definable_finset_biUnion, max_mem_insert_bot_image_coe, finsum_mem_finset_eq_sum, notMem_of_lt_min, Set.Finite.subtypeEquivToFinset_apply_coe, mem_sym2_iff, none_mem_insertNone, prod_lt_one_iff_of_le_one, Bornology.isBounded_biUnion_finset, range_subset, MulAction.mem_stabilizer_finset, Ideal.IsPrime.prod_mem_iff, inf_attach, Bornology.isCobounded_biInter_finset, measurableSet_biInter, Equiv.Perm.support_cycleOf_eq_nil_iff, mem_finsupp_iff_of_support_subset, SimpleGraph.TripartiteFromTriangles.is3Clique_iff, asymptoticCone_biUnion, swap_mem_antidiagonal, mem_of_min, sum_fiberwise_eq_sum_filter, mem_sigma, prod_div_prod_mem_mulSpan, Int.sum_modEq_ite, Affine.Simplex.points_mem_affineSpan_face, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff, Nonempty.csSup_mem, Finsupp.mk_mem_graph_iff, tendsto_indicator_biUnion_finset, Finsupp.zero_notMem_frange, Finpartition.mem_part_ofSetoid_iff_rel, set_biInter_inter, LinearMap.ker_noncommProd_eq_of_supIndep_ker, ProbabilityTheory.iCondIndepSets_singleton_iff, Equiv.Perm.toList_eq_nil_iff, IicProdIoc_def, Finsupp.mem_toMultiset, LocallyFiniteOrderBot.finset_mem_Iio, TwoUniqueSums.uniqueAdd_of_one_lt_card, mem_insert, prod_eq_ite, insert_erase_invOn, SmoothPartitionOfUnity.mem_finsupport, MeasureTheory.SimpleFunc.exists_range_iff, mem_nonMemberSubfamily, set_ncard_biUnion_le, ContextFreeGrammar.Produces.exists_nonterminal_input_mem, Submodule.coe_finsetInf, ProbabilityTheory.iIndepSet.meas_biInter, Absorbs.biUnion_finset, IntermediateField.exists_finset_of_mem_supr'', SSet.stdSimplex.mem_face_iff, ext_iff, Dynamics.coverEntropy_biUnion_finset, UniqueAdd.subsingleton, SimpleGraph.IsFiveWheelLike.notMem_left, mem_upShadow_iterate_iff_exists_card, MeasureTheory.ae_eq_restrict_biUnion_finset_iff, mem_sup_support_iff, sup_eq_top_iff, Finpartition.part_mem, mem_vadd_finset, Profinite.NobelingProof.factors_prod_eq_basis_of_ne, Colex.lt_iff_exists_filter_lt, prod_pow_boole, Topology.CWComplex.cellFrontier_subset_finite_closedCell, set_biInter_insert, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, mem_powers_iff_mem_range_orderOf, Finpartition.mem_part_iff_exists, MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum, UniqueAdd.exists_iff_exists_existsUnique, inf_eq_bot_iff, iInf_biUnion, add_subset_iff, Finsupp.prod_indicator_index_eq_prod_attach, iSup_eq_iSup_finset', Finsupp.prod_eq_zero_iff, not_linearIndependent_iffββ, Colex.toColex_le_toColex, mem_range, Rel.mem_interedges_iff, swap_mem_addAntidiagonal, mem_piAntidiag, add_mem_vadd_finset_iff, mem_imageβ, coe_attach, eventuallyLE_iUnion, filter_eq', mem_image_const_self, sum_dite_eq', MvPolynomial.support_coeff_finSuccEquiv, Function.Injective.mem_finset_image, Equiv.Perm.Basis.mem_support_self, sum_pow_of_commute, exists_mem_empty_iff, Fin.snoc_mem_piFinset_snoc, Subgroup.exists_leftTransversal_of_FiniteIndex, mem_compl, mem_nsmul, SkewMonoidAlgebra.sum_ite_eq', min_mem_image_coe, three_lt_card_iff, iInf_eq_iInf_finset, mulIndicator_biUnion_apply, MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, zero_subset, not_linearIndependent_iffβ, hasSum_iff_compl, Finpartition.part_nonempty, Nat.mem_primeFactors_of_ne_zero, SimpleGraph.IsFiveWheelLike.snd_notMem_left, Finpartition.mem_part_self, SimplexCategory.II.castSucc_mem_finset_iff, Filter.mem_iInf_finset, finsum_mem_finset_product', CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map, Fintype.all_card_le_filter_rel_iff_exists_injective, prod_dite_eq, mem_disjiUnion, mem_neg_vadd_finset_iff, Fintype.complete, three_lt_card, FractionalIdeal.spanFinset_ne_zero, inl_mem_sumLexLift, eventually_cofinite_notMem, eq_singleton_iff_unique_mem, sum_pos_iff_of_nonneg, biInf_finsetSigma, expect_dite_eq', mem_ssubsets, ProbabilityTheory.iCondIndepSet_iff, sum_ite_zero, diag_mem_sym2_mem_iff, Fin.attachFin_uIcc, IsProperSemilinearSet.biUnion_finset, mem_powerset, MeasureTheory.IsSetSemiring.notMem_disjointOfDiff, disjoint_insert_right, Equiv.Perm.zpow_apply_mem_support, isCompact_iff_finite_subfamily_closed, ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul, IntermediateField.exists_finset_of_mem_iSup, inf_set_eq_iInter, addConvolution_ne_zero, inclusion_exclusion_card_biUnion, mem_range_iff_mem_finset_range_of_mod_eq', Topology.CWComplex.mapsTo', Colex.toColex_lt_toColex_iff_exists_forall_lt, Polynomial.one_mem_nthRootsFinset, MeasureTheory.integral_biUnion_eq_sum_powerset, exists_nontrivial_relation_sum_zero_of_not_affine_ind, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, biInf_finsetSigma', SimpleGraph.mk_mem_interedges_iff, mem_union_of_disjoint, mem_powersetCard, sum_sub_sum_mem_addSpan, iInf_finset_image, mem_addSpan, YoungDiagram.mem_cellsOfRowLens, MvPolynomial.mem_support_coeff_optionEquivLeft, SkewMonoidAlgebra.mem_support_iff, AddAction.mem_stabilizer_finset', Finpartition.empty_notMem_parts, codisjoint_right, Seminorm.exists_apply_eq_finset_sup, DFinsupp.notMem_neLocus, Subgroup.finiteIndex_iInf', card_sq_le_card_mul_mulEnergy, zero_notMem_sub_iff, SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton, AddMonoidAlgebra.exists_supDegree_mem_support, Ideal.iSup_iInf_eq_top_iff_pairwise, FreeAbelianGroup.notMem_support_iff, Multipliable.prod_mul_tprod_subtype_compl, ProbabilityTheory.iIndepSets.meas_biInter, Multipliable.tprod_finset_bUnion_disjoint, Equiv.Perm.IsThreeCycle.eq_swap_mul_swap_iff_mem_support, MeasureTheory.Measure.haar.addIndex_defined, le_sup_iff, pimage_subset, mem_map_mk, mem_Ioo, Nat.mem_Ioc_succ', Set.definable_biUnion_finset, ProbabilityTheory.cond_iInter, mem_sdiff, Prime.dvd_finsuppProd_iff, isClopen_biUnion_finset, SimplexCategory.II.last_mem_finset, biUnion_Iic_disjointed, MeasureTheory.VectorMeasure.of_biUnion_finset, Fin.attachFin_Ico, GradedRing.mem_support_iff, orderEmbOfCardLe_mem, MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion, finprod_mem_finset_product', left_mem_uIcc, TopologicalSpace.CompactOpens.coe_finsetSup, Filter.biInter_finset_mem, card_filter_le_iff, SimpleGraph.IsFiveWheelLike.fst_notMem_right, Fintype.expect_ite_mem, sup_inf, exists_mem_eq_sup, prod_attach_univ, Multiset.mem_toEnumFinset, mem_shadow_iff_insert_mem, isWF_bUnion, mem_Ioi, SimpleGraph.swap_mem_interedges_iff, coe_filterMap, IsCompact.elim_nhds_subcover, mem_map_equiv, Polynomial.notMem_support_iff, notMem_uIcc_of_gt, MeasureTheory.ae_restrict_biUnion_finset_iff, notMem_empty, mem_vsub, MvPolynomial.coeff_mul_X', mem_primesOverFinset_iff, mem_div, Equiv.Perm.mem_ofSign, mem_erase, DFinsupp.mem_support_iff, ssubset_iff, AddSubgroup.leftCoset_cover_const_iff_surjOn, Polynomial.Chebyshev.isLocalExtr_T_real_iff, Rel.mk_mem_interedges_iff, Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff, Equiv.Perm.mem_cycleFactorsFinset_conj', YoungDiagram.mk_mem_col_iff, eventuallyEq_iUnion, List.mem_foldr_sup_support_iff, Finsupp.mem_rangeIcc_apply_iff, mem_preimage, mem_of_max, Finpartition.mem_bot_iff, insert_ne_self, image_subset_iff, MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le, AbsolutelyContinuousOnInterval.biUnion_uIoc_subset_of_mem_disjWithin, Sym2.mem_toFinset, isCompact_biUnion, Nonempty.inf_eq_bot_iff, UniqueFactorizationMonoid.mem_primeFactors, Submodule.sum_mem_biSup, right_notMem_Ico, min_eq_bot, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, MvPolynomial.coeff_mem_coeffs, prod_erase_attach, fold_min_le, restrict_preimage_univ, SimpleGraph.CliqueFree.mem_of_sup_edge_isNClique, empty_mem_powerset, FirstOrder.Language.Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset, Equiv.Perm.IsCycle.zpowersEquivSupport_apply, rel_iSup_prod, WithTop.prod_eq_top_iff, card_attach, IsUltrametricDist.exists_norm_finset_sum_le, iInf_union, sum_boole_nsmul, MvPolynomial.mem_support_finSuccEquiv, sup_eq_iSup, some_mem_insertNone, CompositionAsSet.getLast_mem, div_subset_iff, MeasureTheory.ae_restrict_biUnion_finset_eq, card_sq_le_card_mul_addEnergy, IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf, exists_card_fiber_lt_of_card_lt_mul, IsCompact.elim_nhds_subcover_nhdsSet, IsCompact.elim_nhdsWithin_subcover, ProbabilityTheory.iCondIndepSets_iff, mem_toLeft, UniqueAdd.set_subsingleton, mem_inv', prod_extend_by_one, zero_mem_zero, Real.geom_mean_lt_arith_mean_weighted_iff_of_pos, Int.existsUnique_mem_box, Profinite.NobelingProof.spanFinBasis.span, MeasureTheory.Measure.restrict_biUnion_finset, Infinite.exists_notMem_finset, ProbabilityTheory.iIndep_iff, Fin.attachFin_Ioo, Nat.Prime.mem_primeFactors_self, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff', LocallyFiniteOrder.finset_mem_Ico, uIcc_subset_uIcc_iff_mem, Finpartition.card_bind, rel_iSup_sum, Topology.RelCWComplex.cellFrontier_subset_finite_openCell, MeasureTheory.Measure.haar.addIndex_elim, IsCompact.elim_finite_subcover, Nat.mem_antidiagonalTuple, prod_eq_zero_iff, IsNonarchimedean.finset_image_add_of_nonempty, Finsupp.indicator_eq_sum_attach_single, iSup_insert, Equiv.finsetSubtypeComm_symm_apply, UniqueMul.of_card_le_one, diag_mem_sym2_iff, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff', MeasureTheory.addContent_biUnion_eq, SimpleGraph.mem_interedges_iff, Equiv.Perm.pow_apply_mem_support, Nat.Prime.mem_primeFactors, compact_covered_by_add_left_translates, SSet.stdSimplex.objβEquiv_symm_mem_face_iff, card_insert_eq_ite, Multiset.mem_sup, prod_coe_sort_eq_attach, sum_extend_by_zero, IntermediateField.isSplittingField_iSup, sum_neg_iff_of_nonpos, SimpleGraph.mem_neighborFinset, max_eq_top, addConvolution_pos, MonomialOrder.degree_mem_support, prod_attach_eq_prod_dite, finsum_mem_finset_product, SimpleGraph.IsFiveWheelLike.fst_notMem, self_mem_range_succ, Turing.TM2.stmtsβ_self, IsTopologicalBasis.iInf, sUnion_disjiUnion, HasAntidiagonal.mem_antidiagonal, Equiv.Perm.IsThreeCycle.nodup_iff_mem_support, notMem_of_coe_lt_min, Tree.mem_treesOfNumNodesEq_numNodes, exists_mem_ne, MeasureTheory.measure_biUnion_finset_le, FreeAddMonoid.mem_symbols, inter_singleton, YoungDiagram.mem_col_iff, piFinset_filter_const, isPWO_bUnion, mem_sup', CompositionAsSet.zero_mem, IsCompact.elim_nhds_subcover', DFinsupp.mem_pi, prod_ite_mem, inr_mem_sumLiftβ, iInf_singleton, Set.iUnion_eq_iUnion_finset, WithTop.sum_eq_top, mem_disjSum, SimpleGraph.mem_cliqueFinset_iff, sum_ite_mem_eq, Finsupp.notMem_graph_snd_zero, Colex.le_def, SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton, notMem_union, Monoid.exponent_eq_max'_orderOf, isOpen_biInter_finset, mem_bipartiteBelow, filter_ssubset, exists_maximal, mem_falling, MeasureTheory.Measure.restrict_finset_biUnion_congr, Algebra.FiniteType.iff_quotient_mvPolynomial, max'_eq_iff, IsPiSystem.tendsto_probabilityMeasure_biUnion, AddSubgroup.FG.biSup_finset, Nat.prod_modEq_ite, Finpartition.mem_bind, tendsto_tsum_compl_atTop_zero, subset_iff, Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card, Finsupp.mem_support_single, Submodule.iSup_torsionBy_eq_torsionBy_prod, all_card_le_biUnion_card_iff_exists_injective, mem_inf, SimpleGraph.mk_mem_interedges_comm, mulSupport_prod, Ideal.sup_iInf_eq_top, isClopen_biInter_finset, mem_subtype, mem_zmultiples_iff_mem_range_addOrderOf, Behrend.mem_box, IsCompact.elim_nhdsWithin_subcover', notMem_of_max_lt_coe, MeasureTheory.Measure.restrict_biUnion_finset_congr, MeasureTheory.SimpleFunc.mem_restrict_range, isLUB_mem, Finsupp.mem_vaddAntidiagonal_of_addGroup, Topology.CWComplex.cellFrontier_subset_finite_openCell, iInter_mem_sets, exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul, Seminorm.zero_or_exists_apply_eq_finset_sup, Equiv.Perm.pow_apply_mem_toList_iff_mem_support, SimplexCategory.II.mem_finset_iff, Set.definable_biInter_finset, one_lt_prod_iff, Nonempty.attach, right_mem_Icc, IsUltrametricDist.exists_norm_finset_sum_le_of_nonempty, mem_shadow_iterate_iff_exists_card, mem_sumLexLift, left_notMem_Ioc, Fin.attachFin_Iio, SimpleGraph.mem_edgeFinset, Colex.lt_iff_max'_mem, MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion, Tree.mem_treesOfNumNodesEq, sum_pi_single', MeasureTheory.measure_biUnion_finsetβ, exists_mem_image, IntermediateField.exists_finset_of_mem_supr', IsPiSystem.tendsto_measureReal_biUnion, Equiv.Perm.apply_mem_support, mem_shadow_iff_exists_sdiff, ENNReal.exists_le_of_sum_le, Summable.tsum_finset_bUnion_disjoint, Topology.RelCWComplex.mapsTo, empty_mem_ssubsets, notMem_Iio_self, MeasureTheory.measure_biUnion_finset, TopologicalSpace.Clopens.coe_finset_sup, Submodule.mem_iSup_finset_iff_exists_sum, ProbabilityTheory.iCondIndepFun_iff, min'_eq_iff, mem_powersetCard_univ, prod_fiberwise_eq_prod_filter', exists_not_mem_of_card_lt_enatCard, sum_pi_single, Polynomial.natTrailingDegree_mem_support_of_nonzero, inclusion_exclusion_sum_biUnion, exists_card_fiber_le_of_card_le_nsmul, FiniteDimensional.exists_relation_sum_zero_pos_coefficient_of_finrank_succ_lt_card, AddSubmonoid.FG.biSup_finset, coe_notMemRangeEquiv, notMem_sigmaLift_of_ne_left, multipliable_compl_iff, Nat.mem_primeFactors_iff_mem_primeFactorsList, mem_smul_finset, BoxIntegral.unitPartition.mem_prepartition_iff, exists_ne_one_of_prod_ne_one, disjoint_insert_left, support_prod_subset, SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle, Nat.self_notMem_properDivisors, mem_pi, mem_upShadow_iff_exists_sdiff, filter_inj, convexIndependent_iff_finset, card_eq_succ, prod_indicator, Finsupp.sum_attach_index, BoxIntegral.Prepartition.iUnion_def', Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Set.iInter_eq_iInter_finset', prod_ite_eq, SimpleGraph.Walk.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty, ProbabilityTheory.iIndepSet_iff, BoxIntegral.Prepartition.mem_boxes, inl_mem_disjSum, sigma_preimage_mk, finite_cover_nhds_interior, mem_primitiveRoots, Fin.cons_mem_piFinset_cons, Filter.iInf_sets_eq_finite, Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply, notMem_range_self, mem_disjUnion, notMem_of_max_lt, DFinsupp.mem_rangeIcc_apply_iff, subtype_eq_empty, Finsupp.prod_ite_eq, Shatters.exists_superset, mem_add, Equiv.Perm.mem_cycleFactorsFinset_iff, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, exists_lt_of_expect_lt, prod_indicator_const, mem_inf', Int.neg_mem_divisorsAntidiag, mem_compls, inter_insert, image_insert_memberSubfamily, convolution_eq_zero, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff, Turing.PartrecToTM2.trStmtsβ_self, Ideal.isCoprime_biInf, isGLB_mem, UniqueSums.uniqueAdd_of_nonempty, sub_subset_iff, WithTop.top_mem_insertTop, exists_min_image, Int.mem_box, SimpleGraph.exists_of_maximal_cliqueFree_not_adj, Nontrivial.exists_ne, MeasureTheory.IsSetRing.biUnion_mem, BoxIntegral.Prepartition.mem_ofWithBot, exists_mem_eq_sup', SkewMonoidAlgebra.notMem_support_iff, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff', mul_subset_iff, attach_affineCombination_of_injective, prod_ite_mem_eq, disjoint_right, exists_compls_iff, Fin.mem_piFinset_iff_last_init, CompositionAsSet.mem_boundaries_iff_exists_blocks_sum_take_eq, one_notMem_inv_mul_iff, lt_sup_iff, Finpartition.mk_mem_sparsePairs, Function.updateFinset_def, mem_smulAntidiagonal, supIndep_attach, attach_val, Finsupp.supportedEquivFinsupp_apply_support_val, UniqueMul.set_subsingleton, Nat.sum_modEq_ite, mem_inv, inf'_le_iff, Equiv.Perm.mem_finPairsLT, MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated, Finsupp.mem_vaddAntidiagonal_iff, DFinsupp.mk_apply, iSup_finset_image, subset_erase, exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn, mem_perms_of_finset_iff, sups_subset_iff, CompleteLattice.IsCompactElement.exists_finset_of_le_iSup, YoungDiagram.exists_notMem_col, Affine.Simplex.ExcenterExists.signedInfDist_excenter, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff, MvPolynomial.mem_support_coeff_finSuccEquiv, Turing.TM1.stmtsβ_self, mem_upShadow_iff_erase_mem, one_notMem_div_iff, xInTermsOfW_vars_aux, mem_offDiag, mem_filter, Colex.toColex_lt_toColex, inf_eq_iInf, Polynomial.isRoot_prod, not_linearIndepOn_finset_iff, SimpleGraph.mem_finsetWalkLengthLT_iff, ProbabilityTheory.iIndepSet_iff_meas_biInter, two_lt_card, mem_upShadow_iff_exists_mem_card_add_one, set_biUnion_union, prod_indicator_const_apply, mem_union, mem_map', expect_dite_eq, MonomialOrder.notMem_support_of_degree_lt, not_linearIndependent_iff, mem_smul, exists_notMem, mem_toRight, PairReduction.point_mem_finset_logSizeBallSeq, PMF.uniformOfFinset_apply, isConnected_iff_sUnion_disjoint_open, Polynomial.natDegree_mem_support_of_nonzero, hasProd_compl_iff, disjoint_singleton_right, ConvexOn.exists_ge_of_centerMass, Nontrivial.exists_cons_eq, Finmap.mem_keys, UniqueAdd.of_card_le_one, UV.compress_disjoint, ClassGroup.finsetApprox.zero_notMem, inv_smul_mem_iffβ, mem_symmDiff, singleton_inter, not_subset, Equiv.Finset.union_inr, prod_attach, Multiset.mem_sum, set_biUnion_option_toFinset, hasProd_prod_disjoint, disjoint_singleton_left, Metric.AreSeparated.finset_iUnion_left, MeasureTheory.Measure.haar.index_defined, Polynomial.Monic.irreducible_iff_natDegree', diffs_subset_iff, Submodule.mem_iSup_iff_exists_finset, mem_uIcc_of_ge, Nat.mem_factoredNumbers, sum_attach_univ, mem_diffs, Nat.mem_divisors_prime_pow, AddAction.mem_stabilizer_finset, Numbering.mem_prefixed, Ideal.eq_inf_of_isPrime_inf, Fintype.card_filter_piFinset_const, mem_slice, Nat.mem_smoothNumbersUpTo, Equiv.Perm.IsCycle.forall_commute_iff, MvPolynomial.mem_degrees, exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, LocallyFiniteOrder.finset_mem_Ioc, prod_sum, Submodule.mem_sSup_iff_exists_finset, mem_memberSubfamily, mem_imageβ_iff, MeasureTheory.measureReal_biUnion_finset_le, PairReduction.point_logSizeBallSeq_add_one, mem_inv_smul_finset_iffβ, Submodule.finset_inf_coe, ProbabilityTheory.Kernel.iIndepFun.meas_biInter, Polynomial.mem_coeffs_iff, SmoothPartitionOfUnity.mem_fintsupport_iff, not_linearIndepOn_finset_iffβ, Set.iUnion_eq_iUnion_finset', Ideal.subset_union_prime, mem_Ioc, prod_dite_eq', mem_neg, Nonempty.one_mem_div, tprod_subtype, Finpartition.bot_notMem, Equiv.Perm.two_le_length_toList_iff_mem_support, Nonempty.csInf_mem, Fin.mem_piFinset_iff_zero_tail, notMem_erase, exists_eq_insert_iff, IsCompact.elim_nhds_subcover_nhdsSet', two_lt_card_iff, Int.swap_mem_divisorsAntidiag, prod_indicator_biUnion_sub_indicator, mem_multiples_iff_mem_range_addOrderOf, YoungDiagram.mem_mk, Set.biUnion_finsetSigma', Finsupp.mem_support_toFun, Nat.mem_properDivisors, notMem_uIcc_of_lt, mem_Iio, MeasureTheory.measureReal_biUnion_finsetβ, disjoint_left, Equiv.Perm.IsCycle.commute_iff, set_biInter_singleton, Finsupp.mem_graph_iff, Set.mem_toFinset, vadd_mem_vadd_finset_iff, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, lt_fold_max, ProbabilityTheory.Kernel.iIndepSets_singleton_iff, PairReduction.point_logSizeBallSeq_zero, ClassGroup.mem_finsetApprox, AddSubgroup.exists_leftTransversal_of_FiniteIndex, mem_map, mulIndicator_biUnion_finset_eventuallyEq, mem_infs, ENNReal.sum_eq_top, MeasureTheory.addContent_biUnion_le, YoungDiagram.mk_mem_row_iff, coe_notMemRangeEquiv_symm, Fintype.sum_extend_by_zero, covBy_iff_exists_erase, Seminorm.ball_finset_sup_eq_iInter, partialSups_eq_biUnion_range, isClosed_biUnion_finset, Polynomial.rootSet_prod, WithTop.prod_eq_top_ex_top, FreeAbelianGroup.mem_support_iff, Ideal.IsPrime.prod_mem_iff_exists_mem, Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, erase_eq_self, mem_shadow_iff, pi_eq_empty, finprod_mem_finset_productβ, neg_vadd_mem_iff, mem_inter, nontrivial_def, BoxIntegral.Prepartition.iUnion_ofWithBot, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app_eq_sum, PartitionOfUnity.mem_fintsupport_iff, LocallyFinite.exists_finset_nhds_mulSupport_subset, Option.mem_toFinset, NNReal.tendsto_tsum_compl_atTop_zero, mem_shadow_iterate_iff_exists_mem_card_add, Nat.mem_primesBelow, Set.Intersecting.exists_mem_finset, finprod_mem_finset_eq_prod, filter_attach, Ico_subset_biUnion_Ico, fiber_card_ne_zero_iff_mem_image, sum_fiberwise_eq_sum_filter', forall_mem_not_eq', Finsupp.mem_frange, Metric.AreSeparated.finset_iUnion_right, attach_map_val, Nonempty.ciSup_eq_max'_image, attach_empty, SupPrime.le_finset_sup, MeasureTheory.measureReal_biUnion_eq_sum_powerset, Units.mk0_prod, Set.Finite.exists_finset, MeasureTheory.SimpleFunc.mem_range_self, mem_toList, MeasureTheory.SimpleFunc.support_eq, set_biUnion_preimage_singleton, exists_lt_of_sum_lt, iSup_option_toFinset, Nat.Prime.mem_primeFactors', filter_attach', IsLocalization.ideal_eq_iInf_comap_map_away, convolution_pos, Topology.CWComplex.mapsTo, mem_upShadow_iff, Submonoid.FG.biSup_finset, MultilinearMap.map_sub_map_piecewise, exists_signed_sum, smul_subset_iff, finsum_mem_finset_productβ, Matroid.Indep.augment_finset, mem_shadow_iff_exists_mem_card_add_one, UV.mem_compression, mem_finsuppAntidiag', exists_maximalFor, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, sum_coe_sort_eq_attach, SimpleGraph.IsFiveWheelLike.notMem_right, WithTop.some_mem_insertTop, set_biInter_option_toFinset, indicator_biUnion_eq_sum_powerset, mem_bipartiteAbove, Set.biUnion_finsetSigma_univ', GradedAlgebra.mem_support_iff, Equiv.Perm.mem_conj_support, exists_lt_of_prod_lt', AddSubgroup.finiteIndex_iInf', lcm_eq_zero_iff, LocallyFiniteOrderTop.finset_mem_Ioi, piiUnionInter_singleton_left, Rel.swap_mem_interedges_iff, Nat.mem_divisors_self, Int.prod_modEq_ite, MvPolynomial.mem_coeffs_iff, ProbabilityTheory.Kernel.iIndepFun.cond_iInter, IsCompact.elim_finite_subfamily_closed, set_biUnion_insert, mem_neg', iInf_option_toFinset, partiallyWellOrderedOn_bUnion, zero_mem_smul_iff, CompactSpace.elim_nhds_subcover, filter_mem_eq_inter, Equiv.Perm.isInvariant_of_support_le, sum_dite_eq, LocallyFiniteOrderBot.finset_mem_Iic, not_linearIndepOn_finset_iffββ, mem_product, orderEmbOfFin_mem, exists_of_ssubset, gcd_ne_zero_iff, discreteTopology_biUnion_finset, isRoot_of_unity_iff, tsum_subtype, apply_union_le_sum, expect_ite_eq, exists_ne_zero_of_expect_ne_zero, Nat.notMem_primesBelow, UniqueMul.subsingleton, hasSum_compl_iff, support_sum, Set.Finite.subtypeEquivToFinset_symm_apply_coe, FormalMultilinearSeries.mem_compPartialSumTarget_iff, one_lt_card, sum_mul_boole, zero_notMem_neg_add_iff, IsCompact.elim_finite_subfamily_isClosed_subtype, mem_coe, singleton_iff_unique_mem, Nat.prodMk_mem_divisorsAntidiag, MulAction.mem_stabilizer_finset', infs_subset_iff, Finsupp.mem_sym2_support_of_mul_ne_zero, tendsto_tprod_compl_atTop_one, Nat.mem_Ioc_succ, Nat.mem_primeFactors, mem_eraseNone, measurableSet_biUnion, Finsupp.mem_splitSupport_iff_nonzero, mem_attachFin, mem_upShadow_iterate_iff_exists_sdiff, mem_dfinsupp_iff, exists_lt_of_lt_expect, apply_coe_mem_map, Part.mem_toFinset, Multiset.mem_toFinset, Finsupp.notMem_neLocus, Fintype.not_linearIndependent_iffββ, erase_ne_self, mem_powerset_self, PMF.mem_support_uniformOfFinset_iff, Behrend.exists_large_sphere_aux, mem_biUnion, Finsupp.prod_ite_eq', IntermediateField.finiteDimensional_iSup_of_finset', mem_sups, sum_ite_eq, eventually_cocardinal_notMem, Equiv.Perm.OnCycleFactors.kerParam_apply, Down.mem_compression, Prime.dvd_finset_prod_iff, SetTheory.PGame.Domineering.mem_left, expect_ite_eq', mem_generatePiSystem_iUnion_elim', Finpartition.not_isEquipartition, sum_eq_ite, SimpleGraph.TripartiteFromTriangles.Graph.inββ_iff, hasProd_iff_compl, notMem_map_subtype_of_not_property, mem_val, attach_image_val, set_biInter_biUnion, support_prod, mem_addAntidiagonal, WithBot.some_mem_insertBot, Profinite.NobelingProof.factors_prod_eq_basis, mem_def, Metric.AreSeparated.finset_iUnion_left_iff, biUnion_Ioc_disjointed_of_monotone, Seminorm.closedBall_finset_sup_eq_iInter, compact_covered_by_mul_left_translates, WithBot.bot_mem_insertBot, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, exists_mem_eq_inf', prod_fiberwise_eq_prod_filter, filter_eq, FormalMultilinearSeries.mem_compPartialSumSource_iff, zero_mem_box, exists_le_of_sum_le, Equiv.Perm.cycleOf_ne_one_iff_mem_cycleFactorsFinset, AddMonoidAlgebra.supDegree_mem_support, Finsupp.mem_pi, mem_finAntidiagonal, Polynomial.mem_nthRootsFinset, mem_Ico, ClassGroup.exists_mem_finset_approx', fold_op_rel_iff_or, mem_shatterer, mem_prod_list_ofFn, Set.biInter_finsetSigma_univ', not_disjoint_iff, left_mem_Ico, mem_uIcc, exists_mem_notMem_of_card_lt_card, ProbabilityTheory.iIndepSets_singleton_iff, ClassGroup.exists_mem_finsetApprox, Fin.attachFin_Ioc, notMem_compl, iSup_union, notMem_sigmaLift_of_ne_right, biSup_finsetSigma, PairReduction.radius_logSizeBallSeq_zero, mem_insertNone, IsTopologicalBasis.iInf_induced, min_mem_insert_top_image_coe, mem_sum_list_ofFn, CovBy.exists_finset_insert, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map, Holor.sum_unitVec_mul_slice, ssubset_iff_of_subset, interior_iInter, PartitionOfUnity.mem_finsupport, mem_upShadow_iterate_iff_exists_mem_card_add, insert_inter, mem_mul, mulIndicator_biUnion, ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, MeasureTheory.integral_finset_biUnion, SimpleGraph.Walk.exists_mem_support_forall_mem_support_imp_eq, List.mem_fixedLengthDigits_iff
|
instPartialOrder π | CompOp | β |
instSetLike π | CompOp | 1172 mathmath: LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, MeasureTheory.SimpleFunc.coe_range, Fintype.all_card_le_rel_image_card_iff_exists_injective, Function.update_eq_updateFinset, ProbabilityTheory.iIndepSets.piiUnionInter_of_notMem, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', coe_eq_singleton, Equiv.Perm.support_closure_subset_union, Finsupp.range_subset_insert_frange, UV.compress_injOn, AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq, roth_3ap_theorem, coe_sort_coe, RootPairing.GeckConstruction.h_def, rothNumberNat_spec, coe_one, Filter.mem_pi', natCast_le_rank_iff_finset, MeasureTheory.SimpleFunc.sum_measure_preimage_singleton, Ideal.pow_multiset_sum_mem_span_pow, Nat.bijOn_digitsAppend', pairwise_subtype_iff_pairwise_finset, mem_pow, Fintype.coe_image_univ, RootPairing.GeckConstruction.isSl2Triple, Finsupp.mem_supported_support, isOpen_pi_iff, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, Finpartition.isPartition_parts, isUnit_coe, preimage_add_left_singleton, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, RootPairing.Base.span_coroot_support, coe_infs, Summable.sum_add_tsum_compl, RootPairing.Base.cartanMatrixIn_def, MvPolynomial.mem_image_support_coeff_finSuccEquiv, Geometry.SimplicialComplex.convexHull_subset_space, ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem, Equiv.Perm.Basis.injective, Fintype.coe_finsetEquivSet, MeasureTheory.sum_measureReal_singleton, RootPairing.Base.algebraMap_cartanMatrixIn_apply, prod_mulIndicator_subset, Set.subsingleton_toFinset_iff, Equiv.Perm.Basis.toCentralizer_equivariant, Submodule.isInternal_prime_power_torsion_of_pid, IsLinearSet.closure_finset, inf_id_set_eq_sInter, RootPairing.GeckConstruction.instHasTrivialRadical, Finsupp.support_extendDomain_subset, RootPairing.Base.injective_pairingIn, coe_Ico, preimage_mul_left_one, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, coe_eq_empty, Geometry.SimplicialComplex.mem_space_iff, ProbabilityTheory.Kernel.partialTraj_succ_of_le, AddMonoidHom.noncommPiCoprod_apply, IocProdIoc_preimage, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, prod_eq_prod_extend, Geometry.SimplicialComplex.subset_space, MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff, isEmpty_coe_sort, DFinsupp.mapRange_def, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', sigma_image_fst_preimage_mk, AddSubmonoid.mem_closure_finset, finrank_vectorSpan_image_finset_le, neg_filter_univ, multipliable, coe_biUnion, Set.subset_toFinset, ordConnected_range_coe, linearIndepOn_finset_iff, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, Equiv.restrictPreimageFinset_symm_apply_coe, doubling_lt_three_halves, Set.Finite.coeSort_toFinset, Polynomial.monic_restriction, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, RootPairing.Base.cartanMatrix_map_abs, RootPairing.Base.root_mem_span_int, Equiv.Perm.Basis.toCentralizer_apply, SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn, LieAlgebra.IsKilling.rootSystem_coroot_apply, coe_singleton, coe_empty, RootPairing.GeckConstruction.trace_h_eq_zero, disjoint_coe, pairwiseDisjoint_coe, Ideal.exists_finset_card_eq_height_of_isNoetherianRing, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, Geometry.SimplicialComplex.vertices_eq, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff', MvPolynomial.mem_range_map_iff_coeffs_subset, continuous_restrict_apply, Behrend.sphere_subset_preimage_metric_sphere, coe_filter, coe_prod, FirstOrder.Language.Theory.models_iff_finset_models, RootPairing.Base.cartanMatrixIn_nondegenerate, preimage_inr, erase_injOn, Submodule.mem_span_image_iff_exists_fun, Set.Finite.ssubset_toFinset, Multiset.coeEquiv_apply_coe, coeMonoidHom_apply, coe_attachFin, IsSemilinearSet.closure_finset, SemigroupIdeal.fg_iff, Ideal.Factors.fact_ramificationIdx_neZero, Polynomial.evalβ_restriction, Fin.orderIsoTriple_zero, set_biUnion_coe, Function.Embedding.exists_of_card_le_finset, coe_Iic, coe_vadd_finset, coe_eq_pair, summable_mul_prod_iff_summable_mul_sigma_antidiagonal, coe_univ, Finsupp.mem_supported, not_injOn_of_card_image_lt, dimH_coe_finset, RootPairing.Base.cartanMatrix_apply_eq_zero_iff, Equiv.Perm.Basis.mem_support_self', prod_eq_tprod_mulIndicator, MeasureTheory.isProjectiveLimit_nat_iff, MeasureTheory.integral_infinitePi_of_piFinset, SimpleGraph.isMaximumClique_iff, weightedVSubOfPoint_indicator_subset, hasSum_sum_support_of_ne_finset_zero, DFinsupp.mk_neg, isGΞ΄_compl, Equiv.Perm.Basis.sameCycle, sized_compls, Equiv.Perm.OnCycleFactors.kerParam_range_card, Finpartition.disjoint, Polynomial.contentIdeal_def, Finsupp.comapDomain_smul_of_injective, corners_theorem, Polynomial.lift_of_splits, hasProd_prod_support_of_ne_finset_one, Equiv.Perm.OnCycleFactors.kerParam_injective, dimH_zero, Polynomial.restriction_one, Nat.card_eq_finsetCard, Nat.exists_mem_span_nat_finset_of_ge, summable, Set.Infinite.exists_subset_card_eq, measurable_restrict, Nat.antidiagonalEquivFin_symm_apply_coe, coe_nonempty, noncommSum_union_of_disjoint, Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst, DFinsupp.subtypeSupportEqEquiv_apply_coe, RootPairing.Base.linearIndependent_pair_of_ne, MonoidAlgebra.mem_adjoin_support, preimage_mul_left_singleton, SummationFilter.support_eq_limsInf, coe_range, RootPairing.Base.linearIndepOn_coroot, orderIsoOfFin_symm_apply, DirectSum.mk_smul, MeasureTheory.volume_preserving_piFinsetUnion, RootPairing.Base.cartanMatrix_nondegenerate, RootPairing.GeckConstruction.mem_ΟConjLieSubmodule_iff, DirectSum.mk_injective, measurable_restrictβ, inf_id_eq_sInf, prod_indicator_biUnion_finset_sub_indicator, Function.updateFinset_congr, LinearMap.trace_eq_matrix_trace_of_finset, PrimeSpectrum.isCompact_isOpen_iff, coe_powerset, image_mul_left', AddGroup.fg_iff', CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, isLinearSet_iff, linearIndepOn_finset_iffββ, Geometry.SimplicialComplex.convexHull_inter_convexHull, Dynamics.netMaxcard_infinite_iff, MeasureTheory.Measure.isProjectiveLimit_infinitePi, coe_bipartiteBelow, Algebra.adjoin_attach_biUnion, coe_primesOverFinset, Equiv.Perm.IsCycle.commute_iff', Fin.orderIsoSingleton_apply, Ideal.subset_union_prime', ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage, DFinsupp.subtypeDomain_def, FinsetCoe.canLift, op_vadd_stabilizer_of_no_doubling, SimpleGraph.componentComplFunctor_obj, Finsupp.fun_support_eq, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, card_le_one_iff_subsingleton_coe, Set.powersetCard.coe_coe, LocallyFinite.exists_finset_nhds_support_subset, DependsOn.updateFinset, Function.update_updateFinset, MonoidAlgebra.support_gen_of_gen', RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, sum_indicator_eq_sum_inter, not_mulDissociated, DFinsupp.zipWith_def, sum_attach_eq_sum_dite, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj, Fin.orderIsoPair_zero, Polynomial.rootsExpandPowEquivRoots_apply, coe_coeMonoidHom, RootPairing.Base.exists_root_eq_sum_nat_or_neg, Tuple.monotone_proj, pairwise_coprime_iff_coprime_prod, mem_convexHull', Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, restrictβ_preimage, sigmaAntidiagonalEquivProd_symm_apply_snd, Equiv.Perm.isCycleOn_support_cycleOf, finsum_mem_coe_finset, FirstOrder.Ring.lift_genericPolyMap, image_surjOn_powerset, pow_right_strictMonoOn, Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff, Set.Finset.coe_einfsep, coe_sub, Finsupp.span_le_supported_biUnion_support, SimpleGraph.coe_edgeFinset, SimpleGraph.infinite_iff_in_eventualRange, SimpleGraph.extend_finset_to_connected, Fintype.finsetEquivSet_apply, infsep_pos_iff_nontrivial, nontrivial_coe, singleton_subset_set_iff, insert_inj_on, equitableOn_iff_le_le_add_one, coe_cons, Equiv.Perm.cycleFactorsFinset_eq_finset, coe_wcovBy_coe, not_addDissociated, piCongrLeft_comp_restrict, Polynomial.nthRootsFinset_toSet, Geometry.SimplicialComplex.inter_subset_convexHull, SimpleGraph.coe_cliqueFinset, hasSum_support, List.coe_toFinset, Submodule.mem_span_finset, set_biInter_coe, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, corners_theorem_nat, preimage_add_left_zero, Equiv.Perm.coe_support_eq_set_support, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, SSet.stdSimplex.face_eq_ofSimplex, PartitionOfUnity.exists_finset_nhds, partiallyWellOrderedOn, noncommProd_union_of_disjoint, RootPairing.Base.coroot_mem_span_int, finite_toSet_toFinset, centerMass_id_mem_convexHull, Set.Finite.toFinset_subset, coe_coeAddMonoidHom, Polynomial.degree_restriction, centerMass_id_mem_convexHull_of_nonpos, iSup_coe, MeasureTheory.Measure.infinitePi_pi, LinearMap.det_def, coe_erase, OrderEmbedding.coe_birkhoffFinset, SimpleGraph.end_componentCompl_infinite, AffineIndependent.indicator_eq_of_affineCombination_eq, iInf_coe, IntermediateField.fg_adjoin_finset, MeasureTheory.closedCompactCylinders.isCompact, image_add_right, coe_infsep_of_offDiag_nonempty, mulRothNumber_spec, card_sups_iff, AddSubgroup.rank_closure_finset_le_card, toFinset_coe, SimpleGraph.isClique_map_finset_iff, SimpleGraph.isMaximalIndepSet_compl, Module.Basis.reindexFinsetRange_apply, coe_mem, coe_sdiff, IsLocalizedModule.finsetIntegerMultiple_image, preimage_mul_right_one', pairwise_cons', MeasurableEquiv.coe_IicProdIoc_symm, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, isLUB_sup_id, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj, IsNoetherian.range_finsetBasis, Equiv.Finset.union_inl, Set.union_finset_finite_of_range_finite, Polynomial.rootsExpandEquivRoots_apply, Ideal.span_eq_top_iff_finite, bddAbove, Subgroup.leftCoset_cover_const_iff_surjOn, MeasureTheory.Measure.map_piSingleton, Submodule.span_attach_biUnion, Finsupp.mapDomain_injOn, RootPairing.GeckConstruction.lie_h_e, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, IsPrimitiveRoot.injOn_pow, Function.updateFinset_singleton, prod_mulIndicator_subset_of_eq_one, isIrreducible_iff_sInter, FiniteDimensional.span_finset, isGLB_inf, sized_slice, coe_offDiag, coe_pair, LocallyFinite.exists_finset_support, Algebra.Presentation.coeffs_relation_subset_coeffs, mem_insert_coe, PartitionOfUnity.coe_finsupport, MeasureTheory.IsSetSemiring.mem_supClosure_iff, support_of_fiberwise_sum_subset_image, AddSubmonoid.mem_closure_iff_exists_finset_subset, RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply, Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, PartitionOfUnity.exists_finset_nhds_support_subset, coe_Icc, pairwiseDisjoint_smul_iff, Polynomial.exists_image_comap_of_monic, SimpleGraph.neighborFinset_subset_between_union, IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, card_preimage_eq_sum_card_image_eq, IsDedekindDomain.exists_forall_sub_mem_ideal, DyckWord.equivTreesOfNumNodesEq_symm_apply_coe, Part.coe_toFinset, coe_bipartiteAbove, MeasureTheory.Measure.pi_prod_map_IocProdIoc, LinearRecurrence.sol_eq_of_eq_init, MonoidAlgebra.mem_span_support, Cardinal.mk_compl_finset_of_infinite, SummationFilter.HasSupport.eventually_le_support, DFinsupp.filter_def, Subalgebra.fg_adjoin_finset, Equiv.Perm.Basis.card_ofPermHom_support, eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype, tprod_subtype', map_subtype_subset, injOn_of_card_image_eq, MonoidHom.noncommPiCoprod_apply, Polynomial.restriction_zero, MeasureTheory.isProjectiveMeasureFamily_pi, Tuple.graphEquivβ_apply, Equiv.Perm.Basis.ofPermHom_apply, sum_erase_attach, Algebra.essFiniteType_cond_iff, coe_orderIsoOfFin_apply, attach_affineCombination_coe, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map, eq_affineCombination_of_mem_affineSpan_image, nonempty_coe_sort, coe_mul, Nat.pairwise_coprime_pow_primeFactors_factorization, Polynomial.bUnion_roots_finite, Finsupp.coe_neLocus, IsLocalization.finsetIntegerMultiple_image, HahnSeries.SummableFamily.smul_support_subset_prod, Polynomial.Chebyshev.strictAntiOn_node, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, DyckWord.equivTreesOfNumNodesEq_apply_coe, supIndep_iff_pairwiseDisjoint, Module.le_rank_iff_exists_finset, PrimitiveSpectrum.hull_finsetInf, coe_eq_zero, isGreatest_max', Besicovitch.exist_finset_disjoint_balls_large_measure, Submodule.mem_span_iff_exists_finset_subset, Submodule.mem_span_mul_finite_of_mem_mul, Ideal.Factors.isScalarTower, Equiv.Perm.OnCycleFactors.mem_range_toPermHom'_iff, Finpartition.bind_parts, MeasureTheory.IsProjectiveLimit.measure_univ_eq, Algebra.Presentation.coeffs_relation_subset_core, coe_inj, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous, coe_image_subset_range, MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff, IsExposed.sInter, Caratheodory.mem_minCardFinsetOfMemConvexHull, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ΞΉ_app, Polynomial.rootsExpandPowToRoots_apply, RootPairing.GeckConstruction.trace_toEnd_eq_zero, SimpleGraph.neighborFinset_subset_between_union_compl, coe_image, LinearMap.det_eq_det_toMatrix_of_finset, vectorSpan_eq_span_vsub_finset_right_ne, exists_finset_linearIndependent_of_le_finrank, continuous_restrictβ, SupIndep.independent, Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical, prod_coe_sort, FreeCommRing.exists_finset_support, SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet, UniqueAdd.addHom_preimage, DFinsupp.mk_zero, setOf_mem, IsPrimitiveRoot.primitiveRootsPowEquiv_symm_apply_coe, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, Nat.bijOn_ofDigits', Preorder.measurable_frestrictLeβ, Preorder.continuous_frestrictLe, Submonoid.exists_minimal_closure_eq_top, Cardinal.mk_coe_finset, isNoetherian_adjoin_finset, RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing, HallMarriageTheorem.hall_cond_of_restrict, sup'_eq_csSup_image, image_add_right', AddMonoid.closure_finset_fg, RootPairing.Base.chainBotCoeff_eq_zero, AddGroup.rank_spec, ProbabilityTheory.Kernel.partialTraj_le_def, subset_powersetCard_univ_iff, Submodule.fg_span_iff_fg_span_finset_subset, Group.rank_spec, AddSubmonoid.exists_minimal_closure_eq_top, Polynomial.derivativeFinsupp_derivative, MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty, DirectSum.mk_apply_of_notMem, ProbabilityTheory.iCondIndepFun.condIndepFun_finset, intervalGapsWithin_surjOn, isClosed, measurableSet, affineIndependent_iff_indicator_eq_of_affineCombination_eq, prod_apply_dite, Order.exists_orderEmbedding_insert, Algebra.FiniteType.iff_quotient_freeAlgebra, Equiv.piFinsetUnion_right, SimpleGraph.isNIndepSet_iff, coe_sups, MvPolynomial.mem_supported, coe_Ioc, LocallyFinite.exists_finset_mulSupport, Finsupp.comapDomain_surjective, RootPairing.GeckConstruction.span_range_h'_eq_top, Finsupp.comapDomain_mapDomain, coe_Ioo, Nonempty.csSup_mem, invMulSubgroup_eq_mul_inv, addRothNumber_spec, SimpleGraph.isClique_map_finset_iff_of_nontrivial, Fin.orderIsoTriple_one, Tuple.self_comp_sort, Equiv.Finset.union_symm_left, Affine.Simplex.range_face_points, IicProdIoc_def, SeparatedNhds.of_finset_finset, MvPolynomial.coe_coeffs_map, Equiv.Perm.Basis.ofPermHom_mem_centralizer, Set.Finite.coe_toFinset, MeasureTheory.Measure.pi_prod_map_IicProdIoc, MeasureTheory.measurableCylinders_nat, antidiagonal_subtype_ext_iff, partialSups_eq_sUnion_image, Submodule.mem_span_set, singleton_subset_coe, range_orderEmbOfFin, YoungDiagram.isLowerSet, Nonempty.coe_sort, ProbabilityTheory.iIndepFun_iff_finset, Finpartition.exists_enumeration, doubling_lt_two, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map, Submodule.mem_span_finset', Geometry.SimplicialComplex.indep, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, Submodule.IsMinimalPrimaryDecomposition.distinct, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', coe_coeEmb, coe_ssubset, Equiv.Finset.union_symm_right, preimage_compl, coe_attach, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, continuous_restrict, isProperLinearSet_iff, inv_filter_univ, doubling_lt_golden_ratio, Polynomial.rootSet_def, Nonempty.csInf_eq_min', MeasureTheory.partialTraj_const, SimpleGraph.IsNClique.isClique, Equiv.Perm.Basis.mem_support_self, Equiv.Perm.OnCycleFactors.val_centralizer_smul, preimage_mul_right_one, ProbabilityTheory.Kernel.partialTraj_le, MeasureTheory.mem_closedCompactCylinders, AffineIndependent.finrank_vectorSpan_image_finset, Subgroup.exists_leftTransversal_of_FiniteIndex, mem_nsmul, affineCombination_indicator_subset, Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, IsLocalization.map_integerMultiple, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, Subgroup.rank_closure_finset_le_card, PMF.support_ofMultiset, coe_compl, MonoidAlgebra.exists_finset_adjoin_eq_top, pairwise_cons, centroid_univ, MeasureTheory.IsSetSemiring.diff_eq_sUnion', ProbabilityTheory.Kernel.partialTraj_succ_self, Set.Finite.toFinset_ssubset, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map, coe_smul_finset, sum_indicator_subset_of_eq_zero, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image, not_addDissociated_iff_exists_disjoint, infs_self, rank_span_finset_le, DirectSum.mk_apply_of_mem, pi_eq_generateFrom, coe_vadd, RootPairing.GeckConstruction.Ο_mul_h, UniqueMul.mulHom_preimage, measurable_updateFinset, SmoothPartitionOfUnity.coe_finsupport, DFinsupp.erase_def, coe_infsep, Set.powersetCard.coe_finset, exists_orthonormalBasis, RootPairing.GeckConstruction.instIsIrreducible, MeasureTheory.sum_measure_preimage_singleton, inclusion_exclusion_card_biUnion, Equiv.Perm.Basis.toPermHom_apply_toCentralizer, RootPairing.Base.linearIndepOn_root, mem_convexHull, RootPairing.Base.toCoweightBasis_apply, DiscreteQuotient.comp_finsetClopens, SimpleGraph.coe_finsetWalkLength_eq, pairwiseDisjoint_map_sigmaMk, DFinsupp.coe_neLocus, Module.Basis.mem_span_image, measurable_IicProdIoc, BoxIntegral.Prepartition.pairwiseDisjoint, Submodule.mem_span_mul_finite_of_mem_span_mul, Measurable.dependsOn_of_piFinset, hasSum, MvPolynomial.mem_supported_vars, Module.Basis.reindexFinsetRange_repr_self, RootPairing.Base.span_int_root_support, PiNat.cylinder_eq_pi, Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff, Ideal.iSup_iInf_eq_top_iff_pairwise, MvPolynomial.mem_restrictSupport_iff, Equiv.Perm.Basis.ofPermHom_support, Convex.exists_subset_interior_convexHull_finset_of_isCompact, MeasurableEquiv.coe_IicProdIoc, MeasureTheory.IntegrableOn.finset, SubMulAction.fg_iff, MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff, EMetric.pair_reduction, Monoid.closure_finset_fg, Set.toFinset_subset, sum_indicator_subset, coe_neg, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, Nat.mem_Ioc_succ', SimpleGraph.degree_le_between_add, Nonempty.csSup_eq_max', Submodule.mem_span_finite_of_mem_span, Preorder.frestrictLe_apply, convexHull_eq, Preorder.frestrictLeβ_apply, default_singleton, RootPairing.GeckConstruction.ΟConjLieSubmodule_eq_top_iff, finrank_span_finset_le_card, RootPairing.Base.toCoweightBasis_repr_coroot, Set.Finite.subset_toFinset, finprod_mem_coe_finset, Filter.tendsto_finset_preimage_atTop_atTop, DFinsupp.subtypeSupportEqEquiv_symm_apply_coe, card_mul_iff, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, SimpleGraph.IsNIndepSet.isIndepSet, roth_3ap_theorem_nat, coe_eraseNone, isNilpotent_of_finite_tfae, coe_filterMap, SimpleGraph.coe_incidenceFinset, List.zipWith_swap_prod_support', Equiv.Perm.pairwise_commute_of_mem_zpowers, MeasurableSpace.measurableSet_generateFrom_memPartition_iff, IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime_apply_coe, AddSubgroup.leftCoset_cover_const_iff_surjOn, SimpleGraph.IsMaximumClique.isClique, SimpleGraph.cliqueFreeOn_of_card_lt, coe_list_prod, Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff, PMF.support_ofFinset, IsPrimitiveRoot.primitiveRootsPowEquiv_apply_coe, PrimitiveSpectrum.preimage_upperClosure_compl_finset, prod_dite_of_false, Multiset.toEmbedding_coeEquiv_trans, sum_eq_tsum_indicator, hasProd_support, Submodule.span_range_natDegree_eq_adjoin, Fintype.coe_piFinset, List.pairwise_iff_coe_toFinset_pairwise, Set.indicator_pi_one_apply, SimpleGraph.isMaximalClique_compl, coe_eq_univ, Equiv.Perm.subtypePerm_apply_pow_of_mem, Polynomial.map_restriction, sups_subset_self, coe_injective, coe_covBy_coe, prod_erase_attach, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj, restrict_preimage_univ, IsPrimitiveRoot.injOn_pow_mul, PMF.support_uniformOfFinset, preimage_neg, IsApproximateSubgroup.of_small_tripling, Equiv.Perm.IsCycle.zpowersEquivSupport_apply, Submodule.isPrimary_decomposition_pairwise_ne_radical, SimpleGraph.componentCompl_finite, exists_finset_linearIndependent_of_le_rank, Ideal.Factors.liesOver, isLUB_sup', AddMonoidAlgebra.exists_finset_adjoin_eq_top, MeasureTheory.lintegral_finset, sigmaAntidiagonalEquivProd_symm_apply_snd_coe, MeasureTheory.StronglyMeasurable.dependsOn_of_piFinset, MvPolynomial.mem_support_finSuccEquiv, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, MeasurableSpace.measurableSet_generateFrom_countablePartition_iff, Set.toFinset_ssubset, ProbabilityTheory.identDistrib_iff_forall_finset_identDistrib, subset_set_image_iff, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, coe_infsep_of_offDiag_empty, Submodule.spanRank_toENat_eq_iInf_finset_card, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, univ_eq_attach, RootPairing.GeckConstruction.ΟConj_invFun, Ideal.sum_pow_mem_span_pow, Finsupp.finite_vaddAntidiagonal, centroid_mem_convexHull, untrop_sum, coe_nsmul, MeasureTheory.Filtration.piFinset_eq_comap_restrict, Fintype.coe_finsetOrderIsoSet, FractionalIdeal.mem_span_mul_finite_of_mem_mul, Function.updateFinset_univ_apply, AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, not_mulDissociated_iff_exists_disjoint, isLUB_sup, prod_coe_sort_eq_attach, measurable_updateFinset', MeasureTheory.sum_measureReal_preimage_singleton, prod_attach_eq_prod_dite, Equiv.Perm.isPretransitive_of_isCycle_mem, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app, equitableOn_iff, pi_generateFrom_eq, MonoidAlgebra.support_gen_of_gen, centroidWeightsIndicator_def, Equiv.Perm.OnCycleFactors.coe_toPermHom, PointedCone.mem_span_set, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, Cardinal.mk_eq_nat_iff_finset, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, List.support_formPerm_le', dependsOn_restrict, coe_symmDiff, Set.ssubset_toFinset, inf_sSup_eq_iSup_inf_sup_finset, IsNoetherian.coe_finsetBasisIndex, Nat.prod_pow_primeFactors_factorization, measure_zero, RootPairing.GeckConstruction.isNilpotent_f, Tree.coe_treesOfNumNodesEq, pairwiseDisjoint_piAntidiag_map_addRightEmbedding, sum_dite_of_false, forall_coe, RootPairing.GeckConstruction.lie_e_f_same, SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, MeasureTheory.Measure.isProjectiveLimit_infinitePiNat, coeAddMonoidHom_apply, RootPairing.GeckConstruction.Ο_mul_Ο, MeasureTheory.Measure.count_apply_finset, Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull, DFinsupp.lmk_apply, preimage_add_right_singleton, AddMonoidAlgebra.mem_adjoin_support, IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime, linearIndependent_iff_finset_linearIndependent, isPWO, RootPairing.GeckConstruction.ΟConj_toFun, bddBelow, coe_zero, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app, Nontrivial.coe, Set.image_finset_sum_pi, coe_diffs, Ideal.Factors.finrank_pow_ramificationIdx, RootPairing.GeckConstruction.Ο_mul_e, sup_mem_of_nonempty, List.pairwiseDisjoint_consFixedLengthDigits, SimpleGraph.IsMaximumClique.isMaximalClique, RootPairing.GeckConstruction.isNilpotent_e, Dense.diff_finset, ProbabilityTheory.Kernel.partialTraj_self, sigmaAntidiagonalEquivProd_symm_apply_fst, linearIndepOn_finset_iffβ, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, restrictβ_def, convexHull_eq_union_convexHull_finite_subsets, union_support_maximal_linearIndependent_eq_range_basis, Module.FinitePresentation.out, RootPairing.Base.exists_root_eq_sum_int, Submodule.exists_finset_span_eq_linearIndepOn, IntermediateField.exists_finset_of_mem_adjoin, ENNReal.sum_add_tsum_compl, RootPairing.GeckConstruction.h_mem_lieAlgebra, IicProdIoc_preimage, coe_Ioi, FirstOrder.Language.distinctConstantsTheory_eq_iUnion, Function.updateFinset_univ, PiFinsetCoe.canLift, sized_shadow_iff, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq, FractionalIdeal.spanFinset_coe, IntermediateField.adjoin_finset_isCompactElement, eq_affineCombination_subset_iff_eq_affineCombination_subtype, Polynomial.rootsExpandToRoots_apply, Multipliable.prod_mul_tprod_compl, RootPairing.Base.root_mem_or_neg_mem, card_add_iff, RootPairing.Base.toWeightBasis_apply, Polynomial.coeff_restriction, eq_weightedVSub_subset_iff_eq_weightedVSub_subtype, Set.piCongrLeft_comp_restrict, isLowerSet_shatterer, MvPolynomial.mem_coeffsIn_iff_coeffs_subset, coe_eq_one, MvPolynomial.weightedDecomposition.decompose'_eq, isGLB_iff_isLeast, pairwiseDisjoint_vadd_iff, TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact, Submodule.exists_isInternal_prime_power_torsion, inclusion_exclusion_sum_biUnion, Dynamics.netMaxcard_finite_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, preimage_subset, rank_span_of_finset, Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous, IsOfFinAddOrder.multiples_eq_image_range_addOrderOf, pairwise_subtype_iff_pairwise_finset', Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff, MvPolynomial.exists_finset_renameβ, infsep_zero_iff_subsingleton, DFinsupp.mk_add, OrthonormalBasis.span_apply, AddMonoidAlgebra.support_divOf, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, preimage_inv, RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe, Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, Group.fg_iff', card_image_iff, sigma_preimage_mk, Set.encard_coe_eq_coe_finsetCard, MeasureTheory.measurePreserving_piFinsetUnion, Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply, instIsEmpty, coe_pimage, SimpleGraph.isMaximumIndepSet_iff, MeasureTheory.sum_measure_singleton, UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime, SimpleGraph.end_hom_mk_of_mk, Submonoid.mem_closure_finset, MeasureTheory.dependsOn_cylinder_indicator_const, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, coe_div, Geometry.SimplicialComplex.face_subset_face_iff, Submodule.isInternal_prime_power_torsion, Tuple.eq_sort_iff', CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app, coe_Iio, shatterer_eq, Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, prod_dite, Set.instCanLiftFinsetCoeFinite, sup_eq_sSup_image, preimage_mul_left_one', AddAction.stabilizer_coe_finset, Equiv.restrictPreimageFinset_apply_coe, restrict_preimage, RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff, RootPairing.GeckConstruction.lie_h_f, image_add_left', RootPairing.GeckConstruction.Ο_mul_f, ProbabilityTheory.isProjectiveLimit_map, Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq, DFinsupp.mk_of_mem, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_Ο_app, IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe, Equiv.Perm.cycleFactorsFinset_mem_commute, MeasureTheory.Measure.infinitePiNat_map_restrict, prod_finset_coe, Equiv.Perm.OnCycleFactors.toPermHom_apply, card_mul_finset_lt_two, Group.closure_finset_fg, Finsupp.restrictSupportEquiv_symm_single, coe_product, MeasureTheory.closedCompactCylinders.isClosed, card_infs_iff, AddSubmonoid.FG.exists_minimal_closure_eq, MvPolynomial.support_divMonomial, sup'_id_eq_csSup, coe_sym2, RootPairing.Base.toWeightBasis_repr_root, Preorder.measurable_frestrictLe, Set.iUnion_finset_eq_set, Polynomial.degreeLT_eq_span_X_pow, coe_compls, Finpartition.IsEquipartition.exists_partsEquiv, Function.updateFinset_def, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_Ο_app, PolynomialLaw.range_Ο, List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint, MeasureTheory.partialTraj_const_restrictβ, Module.Basis.repr_support_subset_of_mem_span, Finsupp.supportedEquivFinsupp_apply_support_val, coe_inv, RootPairing.Base.coroot_mem_or_neg_mem, RootPairing.GeckConstruction.lie_e_lie_f_apply, MeasureTheory.Filtration.piLE_eq_comap_frestrictLe, Equiv.Perm.subtypePerm_apply_zpow_of_mem, SupIndep.pairwiseDisjoint, DFinsupp.mk_apply, symInsertEquiv_apply_snd_coe, countable_toSet, sigma_preimage_mk_of_subset, invMulSubgroup_eq_inv_mul, measurable_restrict_apply, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, linearIndepOn_iff_linearIndepOn_finset, SimpleGraph.completeBipartiteGraph_isContained_iff, AddGroup.closure_finset_fg, inf_eq_sInf_image, Nonempty.to_subtype, SimpleGraph.isNClique_iff, not_linearIndepOn_finset_iff, Multiset.coeEquiv_symm_apply_fst, card_imageβ_iff, Cardinal.mk_set_eq_nat_iff_finset, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, Submodule.CoFG.sInf, Finsupp.restrictSupportEquiv_apply, FiniteDimensional.exists_is_basis_integral, RootPairing.GeckConstruction.f_lie_v_same, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, Equiv.Perm.Basis.ofPermHomFun_mul, sups_eq_self, Set.exists_finite_iff_finset, inf'_id_eq_csInf, sSupIndep_iff_finite, coe_filter_univ, Polynomial.natDegree_restriction, powerset_card_disjiUnion, Equiv.Finset.union_inr, nodup_map_iff_injOn, IsOfFinOrder.powers_eq_image_range_orderOf, ProbabilityTheory.map_restrict_eq_of_forall_ae_eq, Caratheodory.minCardFinsetOfMemConvexHull_subseteq, isGLB_inf_id, map_subset_iff_subset_preimage, vadd_stabilizer_of_no_doubling, sum_apply_dite, symInsertEquiv_apply_fst, isAddUnit_coe, coe_zpow, AffineIndependent.exists_affineCombination_eq_smul_eq, Finpartition.parts_top_subsingleton, restrict_def, SimpleGraph.degree_le_between_add_compl, Ideal.Factors.finiteDimensional_quotient_pow, finite_toSet, Dynamics.coverMincard_finite_iff, hasProd, AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux, convexHull_eq_union, IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element, RootPairing.Base.span_root_support, PiFinsetCoe.canLift', untrop_sum_eq_sInf_image, AddMonoidAlgebra.support_gen_of_gen, LinearMap.coe_det, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff, sized_falling, op_smul_stabilizer_of_no_doubling, Submodule.mem_sSup_iff_exists_finset, Submonoid.mem_closure_finset', Colex.le_iff_sdiff_subset_lowerClosure, AddMonoidAlgebra.mem_span_support', MeasureTheory.Measure.infinitePi_map_restrict, Equiv.Perm.Basis.cycleOf_eq, not_linearIndepOn_finset_iffβ, inf'_eq_csInf_image, Ideal.subset_union_prime, Module.Finite.span_finset, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer, nullMeasurableSet, DirectSum.support_subset, Nonempty.csInf_mem, coe_map, symInsertEquiv_symm_apply_coe, algebraicIndependent_finset_map_embedding_subtype, measurable_IocProdIoc, HallMarriageTheorem.hall_cond_of_compl, prod_mulIndicator_eq_prod_inter, Polynomial.coeff_restriction', Ideal.Factors.isPrime, Equiv.piFinsetUnion_left, List.support_formPerm_of_nodup', PrimeSpectrum.exists_image_comap_of_finite_of_free, Behrend.threeAPFree_image_sphere, DFinsupp.mk_sub, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, sum_dite_of_true, linearIndependent_finset_map_embedding_subtype, coe_add, Equiv.Perm.pairwise_disjoint_of_mem_zpowers, Turing.TM1to0.tr_supports, preimage_map, Ideal.isPrimary_decomposition_pairwise_ne_radical, Nat.sigmaAntidiagonalTupleEquivTuple_apply, WCovBy.finset_coe, FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem, AddSubgroup.exists_leftTransversal_of_FiniteIndex, Finsupp.support_subset_iff, coe_Ici, intervalGapsWithin_mapsTo, mulSupport_of_fiberwise_prod_subset_image, addDissociated_iff_sum_eq_subsingleton, ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem, Equiv.Perm.CycleType.count_def, iSupIndep_iff_supIndep, exists_sum_eq_one_iff_pairwise_coprime, SimpleGraph.Walk.coe_edges_toFinset, Polynomial.support_restriction, Submodule.finset_span_isCompactElement, SimpleGraph.card_toFinset_mem_edgeFinset, wellFoundedOn, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, preimage_add_left_zero', pairwise_isRelPrime_iff_isRelPrime_prod, Submodule.mem_span_set_iff_exists_finsupp_le_finrank, CovBy.finset_coe, PMF.toOuterMeasure_apply_finset, restrict_comp_piCongrLeft, LocallyFinite.exists_finset_nhds_mulSupport_subset, RootPairing.GeckConstruction.f_mem_lieAlgebra, isTopologicalBasis_pi, RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos, Fin.orderIsoTriple_two, Multiset.coeEquiv_symm_apply_snd_val, filter_attach, coe_zsmul, DFinsupp.eq_mk_support, Set.Finite.exists_finset_coe, Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset, IsLocalizedModule.map_integerMultiple, Module.Basis.reindexFinsetRange_repr, coe_inter, Submodule.mem_set_smul, le_rank_iff_exists_linearIndependent_finset, RootPairing.GeckConstruction.e_mem_lieAlgebra, preimage_add_right_zero, IsDedekindDomain.exists_representative_mod_finset, ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetβ, infs_self_subset, set_biUnion_preimage_singleton, RootPairing.GeckConstruction.lie_h_h, Finsupp.comapDomain_add_of_injective, MeasureTheory.squareCylinders_eq_iUnion_image, isGLB_inf', filter_attach', Nonempty.to_set, IsNonarchimedean.finset_powerset_image_add, coe_insert, Algebra.essFiniteType_iff, card_diffs_iff, Algebra.EssFiniteType.cond, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, sum_coe_sort_eq_attach, weightedVSub_indicator_subset, PartitionOfUnity.exists_finset_nhds', RootPairing.EmbeddedG2.allRoots_subset_range_root, SimpleGraph.componentComplFunctor_map, Polynomial.degreeLE_eq_span_X_pow, AddSubmonoid.mem_closure_finset', Finpartition.IsEquipartition.exists_partPreservingEquiv, piiUnionInter_singleton_left, SimpleGraph.coe_finsetWalkLengthLT_eq, RootPairing.Base.abs_cartanMatrix_apply, MeasureTheory.IsSetSemiring.exists_finpartition_diff, SimpleGraph.IsMaximumIndepSet.isIndepSet, Finsupp.support_indicator_subset, MeasureTheory.SimpleFunc.map_preimage, SimpleGraph.coe_neighborFinset, Orthonormal.exists_orthonormalBasis_extension, coe_smul, Preorder.piCongrLeft_comp_restrictLe, pairwiseDisjoint_pair_insert, PairReduction.iSup_edist_pairSet, not_linearIndepOn_finset_iffββ, Equiv.Perm.OnCycleFactors.kerParam_range_eq, RootPairing.GeckConstruction.h_eq_diagonal, sum_finset_coe, coe_list_sum, MeasureTheory.measurableCylinders.measurableSet, RootPairing.Base.span_int_coroot_support, IsNoetherian.coeSort_finsetBasisIndex, preimage_mul_right_singleton, exists_coe, MeasureTheory.IsSetSemiring.subset_disjointOfDiff, SkewMonoidAlgebra.mem_span_support, MeasureTheory.mem_measurableCylinders, Fintype.card_coe, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj, Ideal.Factors.piQuotientEquiv_mk, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj, ProbabilityTheory.Kernel.partialTraj_zero, SeparatedNhds.of_singleton_finset, image_mul_right', sup_id_eq_sSup, SimpleGraph.edgeFinset_deleteEdges, Module.Basis.mem_span_repr_support, AddMonoidAlgebra.support_gen_of_gen', mem_coe, monotone_preimage, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux, Finsupp.supportedEquivFinsupp_apply_apply, Equiv.Perm.signBijAux_injOn, Submonoid.FG.exists_minimal_closure_eq, Finsupp.nsmul_single_one_image, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, coe_pow, image_add_left, Equiv.Perm.Basis.ofPermHomFun_one, OrderIso.finsetSetFinite_apply_coe, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint, Nat.mod_injOn_Ico, coe_vsub, sum_coe_sort, preimage_add_right_zero', IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, Module.Basis.reindexFinsetRange_self, apply_coe_mem_map, Dynamics.exists_isDynCoverOf_of_isCompact_invariant, IsDedekindDomain.quotientEquivPiFactors_mk, Preorder.piCongrLeft_comp_frestrictLe, coe_sum, sup_id_set_eq_sUnion, coe_imageβ, LinearMap.le_rank_iff_exists_linearIndependent_finset, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, DFinsupp.support_subset_iff, Finsupp.restrictSupportEquiv_symm_apply_coe, AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero, ProbabilityTheory.iIndepFun.indepFun_finsetβ, RootPairing.GeckConstruction.lie_e_f_mul_Ο, MulAction.stabilizer_coe_finset, Preorder.continuous_frestrictLeβ, Polynomial.coeffs_ofSubring, Polynomial.lifts_iff_coeffs_subset_range, Equiv.Perm.OnCycleFactors.kerParam_apply, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff, Set.sized_powersetCard, disjiUnion_Iic_disjointed, Nat.antidiagonalEquivFin_apply_val, mem_generatePiSystem_iUnion_elim', Cardinal.finset_card_lt_aleph0, AddMonoidAlgebra.mem_gradeBy_iff, trop_sInf_image, Matroid.IsRkFinite.exists_finset_isBasis', Submonoid.mem_closure_iff_exists_finset_subset, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, DFinsupp.mk_smul, Tuple.proj_equivβ', preimage_inl, MvPolynomial.supported_eq_vars_subset, Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range, Behrend.threeAPFree_sphere, powersetCard_empty_subsingleton, LieAlgebra.IsKilling.rootSystem_root_apply, exists_cycleOn, Set.ncard_coe_finset, AddMonoidAlgebra.mem_span_support, SimpleGraph.componentCompl_nonempty_of_infinite, coe_subset_singleton, sum_eq_sum_extend, SubAddAction.fg_iff, sigmaAntidiagonalEquivProd_apply, smul_stabilizer_of_no_doubling, Finpartition.part_surjOn, Finpartition.exists_subset_part_bijOn, sigmaAntidiagonalEquivProd_symm_apply_fst, MeasureTheory.Measure.sum_coe_finset, instNonemptyElemCoeInsert, RootPairing.GeckConstruction.e_lie_u, image_mul_left, Fin.orderIsoPair_one, Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom', MeasureTheory.isProjectiveLimit_nat_iff', IntermediateField.induction_on_adjoin_finset, RootPairing.GeckConstruction.lie_e_f_ne, coe_uIcc, Equiv.Perm.OnCycleFactors.centralizer_smul_def, schnirelmannDensity_finset, coe_sigma, isLeast_min', isWF, sum_dite, mem_prod_list_ofFn, piecewise_coe, MeasureTheory.SimpleFunc.map_preimage_singleton, image_mul_right, Ideal.Factors.piQuotientEquiv_map, Set.image_finset_prod_pi, ProbabilityTheory.iIndepFun.indepFun_finset, mulDissociated_iff_sum_eq_subsingleton, AddSemigroupIdeal.fg_iff, MvPolynomial.decomposition.decompose'_eq, Equiv.Perm.commute_ofSubtype_noncommPiCoprod, Set.coe_toFinset, coe_disjUnion, insert_inj_on', LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, RootPairing.Base.chainTopCoeff_eq_of_ne, mem_sum_list_ofFn, nsmul_right_strictMonoOn, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map, coe_union, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply, coe_map_subset_range, prod_dite_of_true, isLUB_iff_isGreatest, DFinsupp.sigmaFinsetFunEquiv_apply_snd_coe, Submodule.spanFinrank_eq_iInf, IsApproximateAddSubgroup.of_small_tripling, tsum_subtype', eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open, coe_subset, Finsupp.image_pow_eq_finsuppProd_image, PMF.toMeasure_apply_finset, Finsupp.sym2_support_eq_preimage_support_mul, HilbertBasis.finite_spans_dense, Polynomial.toSubring_one, Set.definable_iff_finitely_definable
|
partialOrder π | CompOp | 435 mathmath: val_strictMono, toLeft_monotone, bot_eq_empty, pairwiseDisjoint_singleton_iff_injOn, lt_wf, zero_mem_sub_iff, disjoint_insert_erase, disjoint_map, OrderEmbedding.birkhoffFinset_inf, sum_mono_set, card_strictMono, MeasureTheory.GridLines.T_lmarginal_antitone, List.support_formPerm_le, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, instAddLeftMono, Function.Injective.map_atTop_finset_prod_eq, product_self_eq_disjiUnion_perm_aux, tendsto_Ico_neg_atTop_atTop, add_sum_eq_sum_insertNone, pairwiseDisjoint_range_singleton, Icc_eq_image_powerset, grade_eq, isAtom_iff, cauchySeq_finset_iff_nat_tsum_vanishing, CategoryTheory.preservesFiniteColimits_liftToFinset, le_addRothNumber_product, disjoint_erase_insert, DFinsupp.disjoint_iff, disjoint_coe, pairwiseDisjoint_coe, SimpleGraph.isBipartiteWith_neighborFinset_disjoint, disjoint_union_right, Equiv.Perm.support_cycleOf_le, subtype_mono, symmDiff_eq_union_iff, disjoint_filter_filter_neg, monotone_iff_forall_le_cons, card_insertNone, tendsto_Ioc_neg_atTop_atTop, card_Ioo_finset, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt, tendsto_Ioo_atBot_prod_atTop, one_mem_div_iff, antitone_iff_forall_insert_le, exists_disjoint_union_of_even_card, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, mulRothNumber_map_mul_left, disjoint_image, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, disjoint_self_iff_empty, cauchySeq_finset_of_summable_norm, indicator_biUnion_finset_eventuallyEq, tendstoUniformly_tsum_of_cofinite_eventually, SimpleGraph.componentComplFunctor_obj, cauchySeq_finset_iff_nat_tprod_vanishing, Colex.toColex_strictMono, pow_right_monotone, Function.update_updateFinset, Equiv.Perm.support_pow_le, Geometry.SimplicialComplex.isRelLowerSet_faces, Ioo_eq_filter_ssubsets, hasSumUniformly_iff_tendstoUniformly, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj, monotone_iff_forall_le_insert, Finsupp.disjoint_iff, lt_eq_subset, insertNone_eraseNone, pow_right_strictMonoOn, CategoryTheory.preservesFiniteLimits_liftToFinset, MeasureTheory.IsSetSemiring.disjointOfUnion_props, SimpleGraph.infinite_iff_in_eventualRange, coe_wcovBy_coe, erase_wcovBy, cauchySeq_finset_of_norm_bounded_eventually, Profinite.isIso_indexCone_lift, Ico_disjoint_Ico_consecutive, card_eraseNone_le, OrderEmbedding.coe_birkhoffFinset, eraseNone_union, mulRothNumber_spec, eraseNone_none, SimpleGraph.neighborFinset_disjoint_singleton, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, top_eq_univ, zero_mem_neg_add_iff, disjSum_strictMono_left, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj, ENNReal.tendsto_tsum_compl_atTop_zero, PairReduction.disjoint_smallBall_logSizeBallSeq, minimal_iff_forall_diff_singleton, sdiff_eq_self_iff_disjoint, ThreeAPFree.addRothNumber_eq, covBy_iff_exists_cons, WithBot.Ico_bot_coe, OrderIso.finsetSetFinite_symm_apply, cauchySeq_finset_iff_vanishing_norm, card_Iio_finset, addRothNumber_union_le, Equiv.Perm.Disjoint.disjoint_cycleFactorsFinset, hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn, pairwiseDisjoint_smul_iff, Set.disjoint_toFinset, nsmul_right_monotone, SimpleGraph.disjoint_edgeFinset, tendsto_Ioc_atBot_prod_atTop, Ico_eq_filter_ssubsets, card_eraseNone_of_not_mem, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map, covBy_iff_exists_insert, tendsto_mulIndicator_biUnion_finset, codisjoint_left, card_eraseNone_of_mem, Set.pairwiseDisjoint_filter, offDiag_mono, tendsto_Ioo_neg, tendstoUniformlyOn_tsum, Fin.addRothNumber_eq_rothNumberNat, Equiv.finsetCongr_toEmbedding, disjoint_or_nonempty_inter, IsMulFreimanHom.mulRothNumber_mono, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_Ο_app_eq_sum, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ΞΉ_app, card_Icc_finset, one_mem_inv_mul_iff, gc_map_inr_toRight, isCoatom_compl_singleton, Submonoid.exists_minimal_closure_eq_top, SimpleGraph.neighborFinset_boxProd, disjoint_filter, Nat.disjoint_divisors_filter_isPrimePow, FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop, SSet.stdSimplex.face_obj, AddSubmonoid.exists_minimal_closure_eq_top, tendsto_Icc_neg_atTop_atTop, none_mem_insertNone, Numbering.disjoint_prefixed_prefixed, image_some_eraseNone, Filter.tendsto_finset_prod_atTop, mul_prod_eq_prod_insertNone, ThreeGPFree.le_mulRothNumber, tendsto_Ico_atBot_prod_atTop, not_disjoint_iff_nonempty_inter, powersetCard_map, card_union_eq_card_add_card, addRothNumber_spec, dens_strictMono, tendsto_indicator_biUnion_finset, hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn, SimpleGraph.isBipartiteWith_neighborFinset_disjoint', Filter.map_atTop_finset_sum_le_of_sum_eq, Filter.tendsto_finset_powerset_atTop_atTop, IsPrimitiveRoot.disjoint, hasProdLocallyUniformly_iff_tendstoLocallyUniformly, disjoint_iff_ne, covBy_cons, pairwiseDisjoint_iff, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, addRothNumber_le_ruzsaSzemerediNumber, eraseNone_map_some, Ico_eq_image_ssubsets, not_linearIndependent_iffββ, List.disjoint_toFinset_iff_disjoint, coe_coeEmb, Equiv.Perm.ofSign_disjoint, multipliable_iff_cauchySeq_finset, disjSum_mono_right, Equiv.Perm.support_zpow_le, Filter.tendsto_toLeft_atTop, disjoint_filter_filter_not, HasSumUniformly.tendstoUniformly, addRothNumber_empty, rothNumberNat_def, addRothNumber_lt_of_forall_not_threeAPFree, toRight_monotone, Set.Intersecting.disjoint_map_compl, disjoint_map_inl_map_inr, disjoint_Ioi_Iio, card_Ico_finset, Equiv.Perm.support_mul_le, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map, not_addDissociated_iff_exists_disjoint, covBy_iff_card_sdiff_eq_one, monotone_filter_left, disjoint_insert_right, cauchySeq_finset_iff_prod_vanishing, disjoint_sdiff, pairwiseDisjoint_map_sigmaMk, disjiUnion_singleton, codisjoint_right, addRothNumber_singleton, zero_notMem_sub_iff, sum_insertNone, SummationFilter.support_eq_univ_iff, Iic_eq_powerset, cauchySeq_finset_iff_tprod_vanishing, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt, IsMulFreimanIso.mulRothNumber_congr, Fintype.coe_finsetOrderIsoSet_symm, sum_eraseNone, Filter.tendsto_finset_preimage_atTop_atTop, coe_eraseNone, le_mulRothNumber_product, nsmul_right_strictMono, Colex.toColex_mono, Equiv.Perm.support_swap_mul_ge_support_diff, wellFoundedLT, hasProdUniformly_iff_tendstoUniformly, disjoint_range_addLeftEmbedding, instMulRightMono, strictMono_iff_forall_lt_insert, ThreeAPFree.le_addRothNumber, coe_covBy_coe, Filter.tendsto_finset_range, Iic_disjoint_Ioc, some_mem_insertNone, mulRothNumber_empty, tendstoUniformlyOn_tsum_of_cofinite_eventually, isDirected_le, tendsto_Icc_neg, MeasureTheory.Filtration.piFinset_eq_comap_restrict, Fintype.coe_finsetOrderIsoSet, disjoint_iff_inter_eq_empty, not_mulDissociated_iff_exists_disjoint, disjoint_singleton, subset_sdiff, disjoint_filter_filter', Multiset.disjoint_toFinset, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_pt, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app, upShadow_monotone, disjoint_product, isAtom_singleton, sum_anti_set_of_nonpos, addRothNumber_map_add_left, Filter.map_atTop_finset_prod_le_of_prod_eq, pairwiseDisjoint_piAntidiag_map_addRightEmbedding, dens_mono, Ioc_disjoint_Ioc_of_le, Finsupp.support_single_disjoint, tendsto_tsum_compl_atTop_zero, eraseNone_eq_biUnion, Nonempty.not_disjoint, disjoint_biUnion_left, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app, Equiv.Perm.Disjoint.disjoint_support, Equiv.Perm.support_prod_le, prod_mono_set', List.pairwiseDisjoint_consFixedLengthDigits, tendsto_Ioo_neg_atTop_atTop, disjoint_val, sumEquiv_apply_snd, mem_shadow_iterate_iff_exists_card, Fin.addRothNumber_le_rothNumberNat, isLowerSet_shatterer, grade_multiset_eq, ThreeGPFree.mulRothNumber_eq, monotone_sym2, covBy_insert, card_Ioc_finset, pairwiseDisjoint_vadd_iff, le_eq_subset, empty_covBy_singleton, BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitMany, disjoint_empty_right, disjoint_insert_left, prod_eraseNone, exists_disjoint_union_of_even_card_iff, eraseNone_image_some, IsAddFreimanIso.addRothNumber_congr, addRothNumber_le, Equiv.Perm.ofSubtype_eq_iff, card_Iic_finset, Set.Finite.disjoint_toFinset, SimpleGraph.end_hom_mk_of_mk, Nat.disjoint_primeFactors, prod_insertNone, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app, shatterer_eq, instMulLeftMono, IsAddFreimanHom.addRothNumber_mono, WithTop.top_mem_insertTop, shadow_monotone, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_Ο_app, cauchySeq_finset_of_norm_bounded, summable_iff_cauchySeq_finset, insertNone_nonempty, disjoint_right, AddSubmonoid.FG.exists_minimal_closure_eq, cauchySeq_finset_iff_sum_vanishing, one_notMem_inv_mul_iff, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_Ο_app, PairReduction.antitone_logSizeBallSeq_add_one_subset, diag_mono, summable_iff_cauchySeq_finset_and_tsum_mem, Filter.atTop_finset_eq_iInf, univ_option, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, mulRothNumber_le, SimpleGraph.componentComplFunctor_finite, eraseNone_inter, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion, disjoint_sdiff_inter, one_notMem_div_iff, BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_pt, Fintype.finsetOrderIsoSet_toEquiv, disjSum_mono_left, disjoint_biUnion_right, mapEmbedding_apply, SimpleGraph.disjoint_sdiff_neighborFinset_image, disjoint_singleton_right, tendsto_Ico_neg, val_wcovBy_val, powerset_card_disjiUnion, UV.compress_disjoint, Ioc_eq_filter_powerset, disjoint_singleton_left, isCoatom_iff, Iio_eq_ssubsets, instAddRightMono, disjoint_diag_offDiag, Filter.tendsto_finset_Ici_atBot_atTop, strictMono_iff_forall_lt_cons, disjoint_empty_left, tendsto_Ioc_neg, disjoint_box_succ_prod, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, disjoint_filter_and_not_filter, SimpleGraph.componentComplFunctor_nonempty_of_infinite, disjoint_union_left, range_mono, Nat.Coprime.disjoint_primeFactors, WithTop.Ioc_coe_top, disjoint_left, strictAnti_iff_forall_cons_lt, hasProdUniformlyOn_iff_tendstoUniformlyOn, sum_mono_set_of_nonneg, sumEquiv_apply_fst, UniqueFactorizationMonoid.disjoint_primeFactors, image_mono, tendstoUniformly_tsum, mulIndicator_biUnion_finset_eventuallyEq, MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion, Finsupp.support_monotone, covBy_iff_exists_erase, SSet.stdSimplex.face_le_face_iff, addRothNumber_Ico, Equiv.Perm.ofSubtype_support_disjoint, HasProdUniformlyOn.tendstoUniformlyOn, SummationFilter.LeAtTop.le_atTop, hasSumUniformlyOn_iff_tendstoUniformlyOn, HasProdUniformly.tendstoUniformly, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ΞΉ_app_eq_sum, mulRothNumber_lt_of_forall_not_threeGPFree, MvPolynomial.disjoint_support_monomial, NNReal.tendsto_tsum_compl_atTop_zero, tendsto_Icc_atBot_prod_atTop, le_iff_subset, Polynomial.support_scaleRoots_le, Ioc_disjoint_Ioc, disjSum_strictMono_right, addRothNumber_map_add_right, List.zipWith_swap_prod_support, card_eraseNone_eq_card_erase, lt_iff_ssubset, Equiv.Perm.mem_cycleFactorsFinset_support_le, WithTop.some_mem_insertTop, HasSumUniformlyOn.tendstoUniformlyOn, maximal_iff_forall_insert, SimpleGraph.componentComplFunctor_map, BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter, WithTop.Icc_coe_top, subset_compl_iff_disjoint_left, Equiv.Perm.disjoint_iff_disjoint_support, sdiff_disjoint, strictMono_sym2, pow_right_strictMono, Filter.tendsto_finset_Iic_atTop_atTop, mulRothNumber_map_mul_right, disjoint_range_addRightEmbedding, prod_anti_set_of_le_one, Equiv.Perm.support_le_prod_of_mem, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj, SimpleGraph.singleton_disjoint_neighborFinset, zero_notMem_neg_add_iff, SummationFilter.unconditional_filter, Filter.tendsto_toRight_atTop, monotone_preimage, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux, Submonoid.FG.exists_minimal_closure_eq, pairwiseDisjoint_slice, OrderIso.finsetSetFinite_apply_coe, mulRothNumber_union_le, tendsto_tprod_compl_atTop_one, erase_covBy, mem_eraseNone, hasSumLocallyUniformly_iff_tendstoLocallyUniformly, gc_map_inl_toLeft, NonarchimedeanAddGroup.cauchySeq_sum_of_tendsto_cofinite_zero, Function.Injective.map_atTop_finset_sum_eq, Filter.tendsto_finset_image_atTop_atTop, FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop, eraseNone_empty, eraseNone_insertNone, IsAntichain.disjoint_slice_shadow_falling, sumEquiv_symm_apply, cauchySeq_finset_iff_tsum_vanishing, Icc_eq_filter_powerset, antitone_iff_forall_cons_le, cauchySeq_finset_of_geometric_bound, wcovBy_insert, pairwise_disjoint_powersetCard, disjoint_erase_comm, strictAnti_iff_forall_lt_insert, WithBot.some_mem_insertBot, card_mono, WithBot.bot_mem_insertBot, WithBot.Icc_bot_coe, map_some_eraseNone, mul_eq_mul_prime_prod, subset_compl_iff_disjoint_right, OrderEmbedding.birkhoffFinset_sup, not_disjoint_iff, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly, NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one, DFinsupp.support_monotone, disjoint_of_subset_iff_left_eq_empty, mem_insertNone, mulRothNumber_singleton, nsmul_right_strictMonoOn, prod_mono_set_of_one_le', val_covBy_val, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map
|
toSet π | CompOp | β |
val π | CompOp | 135 mathmath: val_strictMono, range_val, insert_val, pimage_eq_image_filter, val_disjSum, Equiv.Perm.cycleType_eq', CovBy.finset_val, BoxIntegral.TaggedPrepartition.filter_boxes_val, val_lt_iff, val_toFinset, Multiset.canLiftFinset, singleton_val, Equiv.finsuppUnique_symm_apply_support_val, disjUnion_val, ordConnected_range_val, sdiff_val, Multiset.bijective_iff_map_univ_eq_univ, biUnion_val, insert_def, map_val_val_powersetCard, dedup_eq_self, MultilinearMap.dfinsuppFamily_apply_support', sort_eq, FiniteField.roots_X_pow_card_sub_X, filterMap_val, insert_val_of_notMem, prod_val, mem_univ_val, sum_val, univ_val_map_subtype_val, val_eq_zero, gcd_def, Multiset.map_fst_le_of_subset_toEnumFinset, cons_val, noncommProd_lemma, union_val_nd, inf_def, insert_val', Subfield.roots_X_pow_char_sub_X_bot, Polynomial.roots_eq_of_degree_le_card_of_ne_zero, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues, nodup, sum_pow_of_commute, Multiset.map_univ_coe, Multiset.map_univ_val_equiv, noncommSum_insert_of_notMem, coe_toList, lcm_def, noncommSum_insert_of_notMem', val_injective, noncommSum_cons, subset_def, Nat.sum_divisors_filter_squarefree, Polynomial.cyclotomic.roots_eq_primitiveRoots_val, sum_eq_multiset_sum, Multiset.map_toEnumFinset_fst, Polynomial.roots_eq_of_degree_eq_card, product_val, prod_map_val, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, univ_val_map_subtype_restrict, Finpartition.ofSetoid_parts_val, inter_val_nd, Multiset.map_univ, noncommProd_cons', SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, Polynomial.roots_prod, ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id, MvPolynomial.aeval_esymm_eq_multiset_esymm, disjoint_val, ConjRootClass.aroots_minpoly_eq_carrier_val, grade_multiset_eq, filter_val, map_val, prod_eq_multiset_prod, Polynomial.Chebyshev.roots_T_real, MvPolynomial.degrees_esymm, AddEquiv.finsuppUnique_symm_apply_support_val, List.toFinset_val, Multiset.map_univ_comp_coe, sum_multiset_singleton, image_val_of_injOn, Matrix.IsHermitian.roots_charpoly_eq_eigenvaluesβ, esymm_map_val, Polynomial.roots_of_cyclotomic, BoxIntegral.TaggedPrepartition.single_boxes_val, union_val, Finmap.keys_val, attach_val, Finsupp.supportedEquivFinsupp_apply_support_val, WCovBy.finset_val, UniqueFactorizationMonoid.primeFactors_val_eq_normalizedFactors, MvPolynomial.esymm_eq_multiset_esymm, Multiset.lists_nodup_finset, val_wcovBy_val, noncommProd_insert_of_notMem', nodup_map_iff_injOn, pi_val, empty_val, Equiv.Perm.cycleType_def, erase_val, sup_def, card_def, Nat.val_divisorsAntidiagonal, noncommSum_cons', Polynomial.roots_eq_of_degree_le_card, card_val, val_univ_fin, Nat.divisors_filter_squarefree, inter_val, sym2_val, sum_map_val, image_val, Fintype.nodup_map_univ_iff_injective, Multiset.count_univ, val_inj, Polynomial.roots_eq_of_natDegree_le_card_of_ne_zero, Finsupp.toMultiset_sum_single, val_le_iff_val_subset, noncommProd_insert_of_notMem, val_le_iff, noncommSum_lemma, mem_val, Polynomial.Chebyshev.roots_U_real, disjiUnion_val, mem_def, noncommProd_cons, Fin.univ_val_map, Finpartition.avoid_parts_val, Polynomial.roots_prod_X_sub_C, val_covBy_val, sort_val, val_eq_singleton_iff, Multiset.toFinset_val, Polynomial.toSubring_one
|