Defs

📁 Source: Mathlib/Data/Finset/Defs.lean

Statistics

Metric	Count
Definitions coeEmb, decidableDExistsFinset, decidableDforallFinset, decidableEq, decidableEqPiFinset, decidableExistsAndFinset, decidableExistsAndFinsetCoe, decidableMem, decidableMem', instDecidableLE, instDecidableLT, instDecidableRelSSubset, instDecidableRelSubset, instHasSSubset, instHasSubset, instPartialOrder, instSetLike, partialOrder, toSet, val, instDecidableMapsToCoeFinsetOfDecidablePredMemSet, instDecidableSurjOnCoeFinsetOfDecidableEq	22
Theorems canLift, canLift, canLift', antisymm, antisymm_iff, refl, rfl, trans, trans, coe_coeEmb, coe_inj, coe_injective, coe_mem, coe_sort_coe, coe_ssubset, coe_subset, eq_of_veq, exists_coe, exists_of_ssubset, ext, ext_iff, forall_coe, forall_mem_not_eq, forall_mem_not_eq', instAntisymmSubset, instAsymmSSubset, instIrreflSSubset, instIsNonstrictStrictOrderSubsetSSubset, instIsTransSSubset, instIsTransSubset, instReflSubset, isWellFounded_ssubset, le_eq_subset, le_iff_subset, lt_eq_subset, lt_iff_ssubset, mem_coe, mem_def, mem_mk, mem_of_subset, mem_val, mk_coe, nodup, notMem_mono, not_mem_subset, not_subset, pairwise_subtype_iff_pairwise_finset, pairwise_subtype_iff_pairwise_finset', setOf_mem, ssubset_def, ssubset_iff_of_subset, ssubset_iff_subset_ne, ssubset_of_ssubset_of_subset, ssubset_of_subset_of_ssubset, subset_def, subset_iff, subset_iff_notMem, subset_of_eq, subset_of_le, val_inj, val_injective, val_le_iff, val_lt_iff, val_strictMono, wellFoundedLT, canLiftFinset	66
Total	88

Finset

Definitions

Name	Category	Theorems
coeEmb 📖	CompOp	1 math math: coe_coeEmb
decidableDExistsFinset 📖	CompOp	—
decidableDforallFinset 📖	CompOp	6 math math: map_nsmul_piAntidiag, prod_ite_zero, Finpartition.mem_atomise, char_dvd_card_solutions_of_sum_lt, prod_boole, nsmul_piAntidiag
decidableEq 📖	CompOp	47 math math: collapse_eq, IsLowerSet.le_card_inter_finset, Icc_eq_image_powerset, UV.shadow_compression_subset_compression_shadow, 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, UV.card_shadow_compression_le, 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 math math: pi_insert
decidableExistsAndFinset 📖	CompOp	—
decidableExistsAndFinsetCoe 📖	CompOp	5 math math: prod_ite_one, expect_ite_zero, Fintype.all_card_le_filter_rel_iff_exists_injective, sum_ite_zero, piFinset_filter_const
decidableMem 📖	CompOp	129 math math: 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, GeneralSchauderBasis.proj_apply_basis_mem, ContinuousMultilinearMap.map_piecewise_add, update_eq_piecewise, Fintype.prod_ite_mem, Fintype.sum_ite_mem, finsuppAntidiagEquivSubtype_symm_apply_coe, sum_fiberwise_eq_sum_filter, ContinuousMultilinearMap.map_add_univ, Int.sum_modEq_ite, alternatingGroup.map_ofSubtype, 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.e_mem_of_eq_true, 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, alternatingGroup.range_ofSubtype, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_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, Profinite.NobelingProof.eval_eq_πJ, Fintype.card_filter_piFinset_const, Equiv.Perm.IsCycle.forall_commute_iff, prod_dite_eq', Profinite.NobelingProof.one_sub_e_mem_of_false, MvPowerSeries.coeff_truncFinset, 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, MvPolynomial.coeff_add_pow, 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, Equiv.Perm.conj_smul_range_ofSubtype, MultilinearMap.map_add_univ, alternatingGroup.ofSubtype_comp_subtype, insert_inter
decidableMem' 📖	CompOp	5 math math: 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	7 math math: UV.shadow_compression_subset_compression_shadow, UV.card_shadow_compression_le, 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 math math: Ioo_eq_filter_ssubsets, Ioc_eq_filter_powerset
instDecidableRelSubset 📖	CompOp	7 math math: 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	64 math math: 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, attachFin_ssubset_attachFin, ssubset_iff_subset_ne, Ioo_eq_filter_ssubsets, Ioi_ssubset_Ioi, lt_eq_subset, ssubset_iff_exists_subset_erase, disjSum_ssubset_disjSum_of_subset_of_ssubset, instIrreflSSubset, isWellFounded_ssubset, instAsymmSSubset, instIsNonstrictStrictOrderSubsetSSubset, ssubset_of_subset_of_ssubset, 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, ssubset_of_ssubset_of_subset, 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, disjSum_ssubset_disjSum_of_ssubset_of_subset, 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	733 math math: Polynomial.supp_subset_range, SimpleGraph.edgeFinset_mono, WittVector.remainder_vars, div_subset_div, disjSups_subset_iff, DFinsupp.support_zipWith, Finsupp.support_finset_sum, MvPolynomial.support_sum, Nonempty.subset_one_iff, filterMap_mono, mul_inter_subset, MvPolynomial.support_mul, image_subset_infs_left, smulAntidiagonal_mono_right, rothNumberNat_spec, union_subset, 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, mul_subset_mul_left, vsub_subset_vsub_left, nsmul_subset_nsmul, 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, diffs_subset_left, 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, filter_subset_filter, Finpartition.parts_subset_extendOfLE, Finpartition.card_parts_equitabilise_subset_le, SimpleGraph.interedges_mono, inter_eq_inter_iff_left, insert_subset_insert, 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, Subset.trans, 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, shatterer_mono, Finsupp.mapDomain_support, Polynomial.support_C_mul_X', smul_finset_subset_smul_finset_iff₀, toLeft_subset_toLeft, Multiset.support_sum_subset, Ioo_subset_Icc_self, ruzsa_covering_mul, ssubset_iff_subset_ne, subset_insert_iff_of_notMem, map_symm_subset, biUnion_mono, support_sum_subset, subset_map_inl, subset_of_le, Subset.refl, image_subset_image_iff, MvPolynomial.coeffs_one, inter_vadd_subset, powersetCard_mono, SimpleGraph.extend_finset_to_connected, insert_subset_iff, ssubset_iff_exists_subset_erase, union_subset_left, Polynomial.support_trinomial', union_eq_left, product_subset_product, subset_add, inter_sub_subset, Icc_subset_Ioc_iff, wittStructureRat_vars, Icc_subset_Icc_left, insert_subset, DFinsupp.support_mk_subset, IsLocalization.integerNormalization_support, 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, pow_subset_pow, MvPolynomial.support_add, inter_subset_inter_right, 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, alternatingGroup.mem_range_ofSubtype_iff, infs_sups_subset_right, product_subset_product_left, card_le_one_iff_subset_singleton, Ico_subset_Ico_left, Nat.primeFactors_mono, subset_div, subset_mul_right, union_subset_union, AddMonoidAlgebra.support_mul_single_subset, univ_subset_iff, Set.Sized.subset_powersetCard_univ, vsub_subset_vsub, 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, inter_subset_inter, Subset.antisymm_iff, instIsNonstrictStrictOrderSubsetSSubset, Ico_eq_filter_ssubsets, AddMonoidAlgebra.support_single_mul_subset, vsub_subset_iff, Finsupp.support_mul_subset_right, addAntidiagonal_mono_right, sub_subset_sub, compls_subset_iff, filter_subset, MvPolynomial.vars_sub_subset, subset_compl_singleton, disjSups_subset_left, vadd_finset_subset_iff, subset_range_sup_succ, union_subset_union_left, 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, sups_subset_right, 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, nsmul_subset_nsmul_left, image_subset_diffs_left, DFinsupp.support_tsub, infs_subset_left, smul_finset_subset_iff₀, subset_powersetCard_univ_iff, Icc_subset_Ico_right, subset_diffs, sym_union, Fintype.piFinset_subset, neg_subset_neg, subset_cons, monotone_filter_right, add_inter_subset, SimpleGraph.incidenceFinset_subset, range_subset, disjSum_mono, SimpleGraph.isBipartiteWith_neighborFinset_subset, smul_subset_smul_right, sym2_mono, add_subset_iff_right, right_eq_union, DFinsupp.support_rangeIcc_subset, disjSups_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, rado_selection, 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, subset_iff_notMem, pow_subset_pow_mul_of_sq_subset_mul, 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, add_subset_add, 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, smul_finset_subset_smul_finset, union_subset_right, 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, biUnion_subset_biUnion_of_subset_left, 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, erase_subset_erase, Preorder.frestrictLe₂_apply, Finsupp.support_mapRange, Set.Finite.subset_toFinset, subset_one_iff_eq, Superset.trans, MvPolynomial.vars_prod, inv_subset_inv, image₂_subset_right, 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, finsuppAntidiag_mono, 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, mul_subset_mul_right, Ioc_subset_Ioi_self, xInTermsOfW_vars_subset, Polynomial.support_integralNormalization_subset, sups_subset_self, smul_subset_smul, 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, union_subset_union_right, 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, image_subset_image, 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, sub_subset_sub_right, 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, shadow_mono, subset_univ_image_iff, Nat.divisors_subset_properDivisors, subset_iff, uIcc_subset_Icc, sdiff_subset_sdiff_iff_subset, Finsupp.support_smul, Ideal.decomposition_erase_inf, Finsupp.support_update_subset, Ico_add_Ioc_subset, Finsupp.eq_indicator_self_iff, toRight_subset_toRight, subset_subsetSum, sigma_mono, subset_sub, pi_subset, prod_powerset_cons, SmoothPartitionOfUnity.finsupport_subset_fintsupport, Ioi_subset_Ioi, image₂_inter_subset_left, map_inr_subset_iff_subset_toRight, vadd_finset_subset_add, sups_subset_left, 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, vadd_subset_vadd_right, Icc_mul_Icc_subset', List.support_sum_subset, Ico_subset_Iio_self, PartitionOfUnity.finsupport_subset_fintsupport, preimage_subset, Iic_add_Iio_subset, Ioi_add_Ici_subset, div_subset_div_left, diffs_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, sdiff_subset_sdiff, 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, sumLexLift_mono, SimpleGraph.edgeFinset_subset_edgeFinset, sub_subset_iff, subset_singleton_iff', pimage_mono, attachFin_subset_attachFin, 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, image₂_subset, subset_erase, support_subset_support_matPolyEquiv, singleton_subset_singleton, div_subset_div_right, biUnion_subset, preimage_subset_of_subset_image, Nonempty.subset_zero_iff, Iio_subset_Iio, sups_subset_iff, MvPolynomial.vars_map, MvPolynomial.support_sub, sumLift₂_mono, 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, image₂_subset_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, pow_subset_pow_left, sub_subset_sub_left, 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, diffs_subset_right, vsub_subset_vsub_right, empty_subset, vadd_finset_subset_vadd, IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic, mul_subset_mul, subset_inter_iff, sups_subset, WittVector.wittNSMul_vars, Icc_add_Ico_subset, MvPolynomial.support_rename_killCompl_subset, exists_eq_insert_iff, MeasureTheory.SimpleFunc.range_const_subset, Nonempty.subset_singleton_iff, subset_smul_finset_iff₀, union_add_inter_subset_union, subset_inter, MvPowerSeries.support_truncFinset_subset, SmoothPartitionOfUnity.eventually_finsupport_subset, Ioo_subset_Ico_self, add_subset_add_left, union_sub_inter_subset_union, powerset_mono, vaddAntidiagonal_mono_right, inter_add_union_subset_union, smul_inter_subset, product_subset_product_right, subset_vsub, LaurentPolynomial.support_C_mul_T, subset_product, inter_vadd_union_subset_union, Ico_subset_Ioo_left, Ioo_subset_Iio_self, subsetSum_mono, subset_disjSum, subset_smul, Rel.interedges_mono, 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, rado_selection_subtype, smul_subset_iff, subset_mul_left, mem_shadow_iff_exists_mem_card_add_one, mem_finsuppAntidiag', MvPolynomial.vars_add_subset, vadd_subset_vadd, sups_inter_subset_left, infs_subset, Ico_mul_Ioc_subset', zero_smul_finset_subset, MvPolynomial.support_symmDiff_support_subset_support_add, PairReduction.pairSet_subset, Set.toFinset_mono, Finpartition.biUnion_filter_atomise, subset_compl_iff_disjoint_left, subset_pow, inter_subset_inter_left, MonoidAlgebra.support_single_mul_subset, zero_smul_subset, disjSups_subset_right, infs_inter_subset_left, zero_mul_subset, insert_erase_subset, Finsupp.support_tsub, not_linearIndepOn_finset_iffₒₛ, subset_union_right, vadd_finset_subset_vadd_finset, smul_zero_subset, sym_mono, inv_subset_div_right, SimpleGraph.isBipartiteWith_neighborFinset_subset', HahnSeries.SummableFamily.support_powerSeriesFamily_subset, SimpleGraph.nonuniformWitness_subset, smul_subset_smul_left, union_smul_inter_subset_union, mul_zero_subset, isDirected_subset, Submodule.decomposition_erase_inf, DFinsupp.support_sum, sdiff_subset, infs_subset_right, 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, exists_subsuperset_card_eq, infs_inter_subset_right, Finsupp.support_zipWith, compl_subset_compl, Behrend.sphere_subset_box, vadd_subset_vadd_left, Ici_subset_Ici, sigmaLift_mono, 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, add_subset_add_right, 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, nsmul_subset_nsmul_add_of_sq_subset_add, coe_subset, mem_upShadow_iterate_iff_exists_mem_card_add, restrict₂_comp_restrict₂
instPartialOrder 📖	CompOp	—
instSetLike 📖	CompOp	2889 math math: Finpartition.mem_part_ofSetSetoid_iff_rel, List.mem_toFinset, LieAlgebra.IsKilling.rootSystem_toLinearMap_apply, iSup_biUnion, MeasureTheory.SimpleFunc.coe_range, Fintype.all_card_le_rel_image_card_iff_exists_injective, Function.update_eq_updateFinset, ProbabilityTheory.iIndepSets.piiUnionInter_of_notMem, SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff', expect_ite_mem, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', MeasureTheory.Measure.pi_pi_finset, coe_eq_singleton, Equiv.Perm.support_closure_subset_union, Finsupp.range_subset_insert_frange, 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, AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq, Colex.mem_initSeg_self, Nonempty.zero_mem_sub, roth_3ap_theorem, coe_sort_coe, RootPairing.GeckConstruction.h_def, set_biInter_finset_image, filter_notMem_eq_sdiff, Nat.mem_properDivisors_prime_pow, noncommSum_add_distrib_aux, IndepMatroid.ofFinset_indep, rothNumberNat_spec, collapse_eq, 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, coe_one, Submodule.exists_finset_of_mem_iSup, Finpartition.mem_part_iff_part_eq_part, Finsupp.mem_support_iff, finrank_span_finset_eq_card, exists_next_left, Filter.mem_pi', zero_mem_sub_iff, Int.mem_divisorsAntidiag, Nat.coe_properDivisors_eq_prod_pow_lt_factorization, natCast_le_rank_iff_finset, Fintype.mem_piFinset, RootPairing.GeckConstruction.instIsCartanSubalgebraSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', Equiv.Perm.mem_toList_iff, exists_card_fiber_lt_of_card_lt_nsmul, MeasureTheory.SimpleFunc.sum_measure_preimage_singleton, smul_mem_smul, Ideal.pow_multiset_sum_mem_span_pow, Nat.bijOn_digitsAppend', pairwise_subtype_iff_pairwise_finset, mem_pow, mem_zpowers_iff_mem_range_orderOf, Fintype.coe_image_univ, mem_univ, RootPairing.GeckConstruction.isSl2Triple, Filter.frequently_exists_finset, MvPolynomial.exists_finset_rename, Metric.AreSeparated.finset_iUnion_right_iff, Finsupp.mem_supported_support, isOpen_pi_iff, exists_mem_eq_inf, finite_cover_nhds, sum_ite_mem, set_biUnion_biUnion, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, exists_one_lt_of_prod_one_of_exists_ne_one', disjUnion_singleton, Finpartition.isPartition_parts, zero_mem_subsetSum, isUnit_coe, preimage_add_left_singleton, mk_mem_sym2_iff, inv_smul_mem_iff, WithBot.sum_eq_bot_iff, Equiv.Perm.Disjoint.mem_imp, attach_cons, Equiv.Perm.mem_cycleFactorsFinset_conj, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, Set.Sized.shadow_iterate, closure_biUnion, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, RootPairing.Base.span_coroot_support, coe_infs, MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion, Summable.sum_add_tsum_compl, RootPairing.Base.cartanMatrixIn_def, MvPolynomial.mem_image_support_coeff_finSuccEquiv, sum_boole_mul, mem_sumLift₂, disjiUnion_filter_eq, Geometry.SimplicialComplex.convexHull_subset_space, Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt, product_self_eq_disjiUnion_perm_aux, SupIndep.attach, ProbabilityTheory.iCondIndepSets.piiUnionInter_of_notMem, le_fold_max, AntivaryOn.sum_smul_lt_sum_comp_perm_smul_iff, MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion, Equiv.Perm.Basis.injective, Fintype.coe_finsetEquivSet, mem_singleton, 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, MvPolynomial.coeff_X_mul', inf_id_set_eq_sInter, Set.biUnion_finsetSigma, RootPairing.GeckConstruction.instHasTrivialRadical, YoungDiagram.mem_row_iff, IsLocalization.smul_mem_finsetIntegerMultiple_span, mem_dfinsupp_iff_of_support_subset, Finsupp.support_extendDomain_subset, eq_univ_iff_forall, mem_range_iff_mem_finset_range_of_mod_eq, ProbabilityTheory.Kernel.iIndep.meas_biInter, univ_pi_univ, RootPairing.Base.injective_pairingIn, Fin.attachFin_Iic, coe_Ico, indicator_biUnion, preimage_mul_left_one, pairwiseDisjoint_disjUnion, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, coe_eq_empty, Geometry.SimplicialComplex.mem_space_iff, ProbabilityTheory.Kernel.partialTraj_succ_of_le, attach_eq_univ, AddMonoidHom.noncommPiCoprod_apply, subset_mul, IocProdIoc_preimage, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero, mem_image_const, RootPairing.GeckConstruction.h_mem_cartanSubalgebra, InfPrime.finset_inf_le, prod_eq_prod_extend, SimpleGraph.CompleteEquipartiteSubgraph.isCompleteBetween, Geometry.SimplicialComplex.subset_space, left_mem_Icc, MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff, isEmpty_coe_sort, DFinsupp.mapRange_def, mem_upShadow_iff_exists_mem_card_add, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', forall_mem_not_eq, PairReduction.point_notMem_finset_logSizeBallSeq_add_one, le_sup'_iff, ProbabilityTheory.Kernel.condExp_traj', sigma_image_fst_preimage_mk, AddSubmonoid.mem_closure_finset, exists_ne_zero_of_sum_ne_zero, Nat.swap_mem_divisorsAntidiagonal, singleton_disjUnion, Nat.mem_factoredNumbers', ProbabilityTheory.iIndepFun_iff, exists_equiv_extend_of_card_eq, fold_min_lt, finrank_vectorSpan_image_finset_le, Finsupp.mem_frange_of_mem, ProbabilityTheory.iIndep.meas_biInter, mem_singleton_self, neg_filter_univ, multipliable, finsuppAntidiagEquivSubtype_apply_coe, sigma_nonempty, coe_biUnion, set_biUnion_insert_update, Set.subset_toFinset, ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, ordConnected_range_coe, Nat.mem_finMulAntidiag, YoungDiagram.mem_cells, linearIndepOn_finset_iff, Set.Intersecting.isUpperSet', Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, Equiv.restrictPreimageFinset_symm_apply_coe, mk_mem_sigmaLift, mem_of_mem_inter_left, doubling_lt_three_halves, Set.Finite.coeSort_toFinset, left_notMem_Ioo, ProbabilityTheory.Kernel.trajContent_cylinder, MeasureTheory.Measure.ae_mem_finset_iff, Filter.mem_iInf_finite, Polynomial.monic_restriction, MeasureTheory.lintegral_biUnion_finset₀, LieAlgebra.IsKilling.instIsReducedSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, AntivaryOn.sum_mul_eq_sum_mul_comp_perm_iff, IsPrimitiveRoot.mem_nthRootsFinset, Finsupp.if_mem_support, RootPairing.Base.cartanMatrix_map_abs, AddMonoidAlgebra.coeff_comapDomain, MeasureTheory.exists_nonempty_inter_of_measureReal_univ_lt_sum_measureReal, ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul, RootPairing.Base.root_mem_span_int, Nat.one_mem_properDivisors_iff_one_lt, IsSemilinearSet.biUnion_finset, Equiv.Perm.Basis.toCentralizer_apply, LocallyFiniteOrder.finset_mem_Icc, Equiv.Perm.notMem_support, inf_lt_iff, SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn, LieAlgebra.IsKilling.rootSystem_coroot_apply, vadd_mem_vadd, coe_singleton, Finsupp.comapDomain_embDomain, MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen, mem_sym_iff, Equiv.Perm.perm_symm_on_of_perm_on_finset, coe_empty, Nat.coe_divisors_eq_prod_pow_le_factorization, ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussian, IsPiSystem.biInter_mem, SimpleGraph.TripartiteFromTriangles.rel_iff, RootPairing.GeckConstruction.trace_h_eq_zero, Nonempty.exists_mem, SimpleGraph.IsNClique.exists_not_adj_of_cliqueFree_succ, SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq, disjoint_coe, pairwiseDisjoint_coe, set_encard_biUnion_le, Ideal.exists_finset_card_eq_height_of_isNoetherianRing, convolution_ne_zero, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, mem_shadow_iterate_iff_exists_sdiff, Geometry.SimplicialComplex.vertices_eq, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, Nat.prod_mem_factoredNumbers, Set.finite_mem_finset, LieIdeal.reflectionPerm_mem_rootSet_iff, sum_card_fiberwise_eq_card_filter, Fin.mem_piFinset_iff_pivot_removeNth, Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe, 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, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff', Turing.TM1.step_supports, MvPolynomial.mem_range_map_iff_coeffs_subset, continuous_restrict_apply, MvPolynomial.notMem_support_iff, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj', Behrend.sphere_subset_preimage_metric_sphere, mem_cons_of_mem, coe_filter, ciSup_eq_max'_image, coe_prod, FirstOrder.Language.Theory.models_iff_finset_models, RootPairing.Base.cartanMatrixIn_nondegenerate, preimage_inr, erase_injOn, Submodule.mem_span_image_iff_exists_fun, MonovaryOn.sum_smul_comp_perm_lt_sum_smul_iff, IsLocalization.lift_mem_adjoin_finsetIntegerMultiple, BoxIntegral.unitPartition.mem_admissibleIndex_iff, Set.Finite.ssubset_toFinset, Set.Infinite.exists_notMem_finset, Nonempty.sup_eq_top_iff, Finsupp.eq_indicator_iff, DFinsupp.mem_neLocus, Multiset.coeEquiv_apply_coe, right_mem_Ioc, inf'_lt_iff, coeMonoidHom_apply, coe_attachFin, isIrreducible_iff_sUnion_isClosed, IsSemilinearSet.closure_finset, SemigroupIdeal.fg_iff, one_mem_one, prod_ite_one, Rel.mk_mem_interedges_comm, attach_nonempty_iff, DFinsupp.prod_eq_zero_iff, Ideal.Factors.fact_ramificationIdx_neZero, Colex.toColex_lt_toColex_iff_max'_mem, Polynomial.eval₂_restriction, Fin.orderIsoTriple_zero, Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, set_biUnion_coe, Function.Embedding.exists_of_card_le_finset, MeasureTheory.lintegral_biUnion_finset, AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, coe_Iic, lt_sup'_iff, coe_vadd_finset, coe_eq_pair, summable_mul_prod_iff_summable_mul_sigma_antidiagonal, mem_insert_self, AntivaryOn.sum_comp_perm_smul_eq_sum_smul_iff, coe_univ, mem_finsuppAntidiag, setOf_liouvilleWith_subset_aux, mem_sup, Finsupp.mem_supported, UpperHalfPlane.prod_eq_zero_iff, prod_preimage_of_bij, LieModule.genWeightSpaceChain_def', MeasureTheory.Measure.ae_mem_finset_iff_map_eq_sum_dirac, mem_mk, not_injOn_of_card_image_lt, dimH_coe_finset, nullMeasurableSet_biUnion, 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, mem_uIcc', Polynomial.map_mem_nthRootsFinset, weightedVSubOfPoint_indicator_subset, SimpleGraph.regularityReduced_adj, hasSum_sum_support_of_ne_finset_zero, isLindelof_biUnion, MeasureTheory.Measure.haar.index_elim, nsmul_mem_nsmul, le_sup'_of_le, DFinsupp.mk_neg, isGδ_compl, Equiv.Perm.Basis.sameCycle, mem_Ici, sized_compls, biUnion_range_succ_disjointed, AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux, Equiv.Perm.OnCycleFactors.kerParam_range_card, Filter.iInf_principal_finset, SummationFilter.eventually_mem_or_not_mem, inf_le_iff, set_biUnion_finset_image, Dynamics.IsDynCoverOf.iterate_le_pow, Finpartition.disjoint, Polynomial.contentIdeal_def, sum_ite_eq', Finsupp.comapDomain_smul_of_injective, HallMarriageTheorem.hall_hard_inductive, corners_theorem, Polynomial.lift_of_splits, ProbabilityTheory.Kernel.traj_map_updateFinset, Colex.le_iff_max'_mem, notMem_sdiff_of_notMem_left, subset_set_biUnion_of_mem, hasProd_prod_support_of_ne_finset_one, indicator_biUnion_apply, Equiv.Perm.OnCycleFactors.kerParam_injective, dimH_zero, IsSemilinearSet.biInter_finset, IsStrictOrderedRing.int_mem_Icc_of_mul_mem_Ioo, Polynomial.restriction_one, Nat.card_eq_finsetCard, one_mem_div_iff, Equiv.Perm.mem_support_iff_of_commute, Nat.exists_mem_span_nat_finset_of_ge, summable, IsLowerSet.memberSubfamily, Set.Infinite.exists_subset_card_eq, measurable_restrict, finprod_mem_finset_product, Nat.antidiagonalEquivFin_symm_apply_coe, Equiv.Perm.mem_support_ofSubtype, coe_nonempty, noncommSum_union_of_disjoint, MeasureTheory.lintegral_restrict_infinitePi, Nat.sigmaAntidiagonalTupleEquivTuple_symm_apply_fst, DFinsupp.subtypeSupportEqEquiv_apply_coe, ProbabilityTheory.Kernel.map_partialTraj_succ_self, UniqueMul.exists_iff_exists_existsUnique, mem_image_univ_iff_mem_range, SchauderBasis.range_proj_eq_span, RootPairing.Base.linearIndependent_pair_of_ne, MonoidAlgebra.mem_adjoin_support, swap_mem_mulAntidiagonal, inr_mem_sumLexLift, DFinsupp.mem_support_toFun, preimage_mul_left_singleton, inter_mem_infs, SummationFilter.support_eq_limsInf, mem_generatePiSystem_iUnion_elim, set_biInter_insert_update, Fintype.card_filter_piFinset_eq, coe_range, Ioc_subset_biUnion_Ioc, RootPairing.Base.linearIndepOn_coroot, orderIsoOfFin_symm_apply, DirectSum.mk_smul, MeasureTheory.instSFiniteForallValNatMemFinsetInducedFamilyOfForallIic, Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag, MeasureTheory.volume_preserving_piFinsetUnion, RootPairing.Base.cartanMatrix_nondegenerate, addConvolution_eq_zero, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff, Fintype.prod_extend_by_one, RootPairing.GeckConstruction.mem_ωConjLieSubmodule_iff, biUnion_nonempty, SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff', mem_image, Nat.mem_properDivisors_iff_exists, Finpartition.mk_mem_nonUniforms, 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, IsNonarchimedean.finset_image_add, summable_compl_iff, coe_powerset, Nat.eq_prod_primes_mul_sq_of_mem_smoothNumbers, image_mul_left', SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff', eventuallyEq_iInter, AddGroup.fg_iff', CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso_aux_assoc, isLinearSet_iff, Fintype.piFinset_update_eq_filter_piFinset_mem, linearIndepOn_finset_iffₒₛ, Equiv.Perm.IsThreeCycle.support_eq_iff_mem_support, Colex.lt_iff_exists_forall_lt, Geometry.SimplicialComplex.convexHull_inter_convexHull, CovBy.exists_finset_erase, MultilinearMap.map_piecewise_sub_map_piecewise, Dynamics.netMaxcard_infinite_iff, Polynomial.natDegree_notMem_eraseLead_support, Equiv.Perm.SameCycle.mem_support_iff, Algebra.EssFiniteType.adjoin_mem_finset, IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf, MeasureTheory.Measure.isProjectiveLimit_infinitePi, Set.biUnion_finsetSigma_univ, coe_bipartiteBelow, expect_ite_zero, Algebra.adjoin_attach_biUnion, isProperSemilinearSet_iff, coe_primesOverFinset, Equiv.Perm.IsCycle.commute_iff', Fin.orderIsoSingleton_apply, subset_sups, Ideal.subset_union_prime', ProbabilityTheory.IsGaussianProcess.hasGaussianLaw, mem_mulAntidiagonal, TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage, Fin.insertNth_mem_piFinset_insertNth, min'_le, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf, Finsupp.notMem_support_iff, DFinsupp.subtypeDomain_def, LieIdeal.toInvtRootSubmodule_mono, indicator_biUnion_finset_eventuallyEq, iInf_eq_iInf_finset', vsub_mem_vsub, MonomialOrder.degree_mem_support_iff, sdiff_eq_filter, ENNReal.tsum_biUnion_le, FinsetCoe.canLift, mem_sort, op_vadd_stabilizer_of_no_doubling, Prime.exists_mem_finset_dvd, SimpleGraph.componentComplFunctor_obj, Finsupp.fun_support_eq, ExpGrowth.expGrowthSup_sum, ConcaveOn.exists_le_of_centerMass, DFinsupp.notMem_support_iff, zero_mem_smul_finset_iff, Submodule.fg_biSup, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, IsLocalization.coeffIntegerNormalization_mem_support, card_le_one_iff_subsingleton_coe, Set.powersetCard.coe_coe, MeasureTheory.piContent_cylinder, LocallyFinite.exists_finset_nhds_support_subset, DependsOn.updateFinset, MeasureTheory.SimpleFunc.mem_range, Function.update_updateFinset, erase_injOn', MonoidAlgebra.support_gen_of_gen', RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, SimpleGraph.CompleteEquipartiteSubgraph.disjoint, sum_indicator_eq_sum_inter, MvPolynomial.mem_vars, not_mulDissociated, Polynomial.mem_support_derivative, Polynomial.map_mem_nthRootsFinset_one, frequently_exists, MeasureTheory.integrableOn_finset_iUnion, LinearMap.iInf_ker_proj_le_iSup_range_single, Filter.iInf_sets_eq_finite', mem_finsuppAntidiag_insert, MvPolynomial.support_killCompl, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj'', filter_nonempty_iff, DFinsupp.zipWith_def, sum_attach_eq_sum_dite, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj, Fin.orderIsoPair_zero, Polynomial.rootsExpandPowEquivRoots_apply, coe_coeMonoidHom, IntermediateField.finiteDimensional_iSup_of_finset, Colex.mem_initSeg, MeasureTheory.FiniteMeasure.restrict_biUnion_finset, RootPairing.Base.exists_root_eq_sum_nat_or_neg, Tuple.monotone_proj, pairwise_coprime_iff_coprime_prod, mem_convexHull', attach_eq_empty_iff, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, exists_ne_map_eq_of_card_lt_of_maps_to, smul_mem_smul_finset_iff, mem_of_mem_cons_of_ne, restrict₂_preimage, Set.biInter_finsetSigma', mem_zero, sigmaAntidiagonalEquivProd_symm_apply_snd, Nat.mem_divisors, Equiv.Perm.isCycleOn_support_cycleOf, Finpartition.mem_avoid, insert_eq_self, card_erase_eq_ite, sup_set_eq_biUnion, ProbabilityTheory.Kernel.iIndepSet.meas_biInter, smul_mem_smul_finset_iff₀, finsum_mem_coe_finset, FirstOrder.Ring.lift_genericPolyMap, sum_pos_iff, image_surjOn_powerset, ProbabilityTheory.iCondIndep_iff, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, uniqueAdd_of_twoUniqueAdd, max'_mem, pow_right_strictMonoOn, 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, 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, FormalMultilinearSeries.compPartialSumTargetSet_image_compPartialSumSource, attach_insert, Fintype.finsetEquivSet_apply, infsep_pos_iff_nontrivial, nontrivial_coe, singleton_subset_set_iff, mem_vadd, insert_inj_on, insert_subset_iff, ssubset_iff_exists_subset_erase, mem_uIcc_of_le, equitableOn_iff_le_le_add_one, coe_cons, SimpleGraph.notMem_neighborFinset_self, Equiv.Perm.cycleFactorsFinset_eq_finset, prod_indicator_apply, coe_wcovBy_coe, nullMeasurableSet_biInter, not_addDissociated, iInf_insert, disjiUnion_disjiUnion, piCongrLeft_comp_restrict, Profinite.NobelingProof.fin_comap_jointlySurjective, MeasureTheory.integral_biUnion_finset, Polynomial.nthRootsFinset_toSet, compl_mem_compls, Geometry.SimplicialComplex.inter_subset_convexHull, UpperSemicontinuousOn.inter_biInter_preimage_Ici_eq_empty_iff_exists_finset, LinearMap.isLowerSet_support_singularValues, Colex.toColex_le_toColex_iff_max'_mem, count_coe_finsuppAntidiagEquiv_apply, SimpleGraph.coe_cliqueFinset, exists_minimal, hasSum_support, List.coe_toFinset, Submodule.mem_span_finset, Equiv.Perm.commute_iff_of_mem_cycleFactorsFinset, RingHom.locally_iff_isLocalization, subset_add, set_biInter_coe, Finsupp.sum_ite_eq, PairReduction.point_mem_logSizeBallSeq_init, inv_mem_inv, mem_vaddAntidiagonal, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, ProbabilityTheory.uniformOn_apply_finset, corners_theorem_nat, preimage_add_left_zero, Equiv.Perm.coe_support_eq_set_support, Module.exists_nontrivial_relation_of_finrank_lt_card, Profinite.NobelingProof.GoodProducts.spanFin, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq_of_subset, Set.Sized.upShadow, Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, Finsupp.mem_rangeSingleton_apply_iff, SSet.stdSimplex.face_eq_ofSimplex, PartitionOfUnity.exists_finset_nhds, partiallyWellOrderedOn, mem_filter_univ, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, noncommProd_union_of_disjoint, RootPairing.Base.coroot_mem_span_int, Set.biInter_finsetSigma, finite_toSet_toFinset, centerMass_id_mem_convexHull, Int.prodMk_mem_divisorsAntidiag, Set.Finite.toFinset_subset, coe_coeAddMonoidHom, Polynomial.degree_restriction, absorbs_biUnion_finset, eventuallyLE_iInter, centerMass_id_mem_convexHull_of_nonpos, iSup_coe, IsCompact.exists_finite_cover_smul, MeasureTheory.Measure.infinitePi_pi, LinearMap.det_def, Polynomial.mul_mem_nthRootsFinset, SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff, inr_mem_disjSum, Dynamics.IsDynCoverOf.preimage, LieAlgebra.Basis.linearIndepOn_root_baseSupp, Equiv.Perm.mem_support_cycle_of_cycle, inf_sup, coe_erase, OrderEmbedding.coe_birkhoffFinset, AffineIndependent.affineSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one, SimpleGraph.end_componentCompl_infinite, vadd_subset_iff, Equiv.Perm.mem_support, Set.biUnion_empty_finset, hasSum_sum_disjoint, AffineIndependent.indicator_eq_of_affineCombination_eq, iInf_coe, iSup_singleton, SupIrred.finset_sup_eq, IntermediateField.fg_adjoin_finset, MeasureTheory.closedCompactCylinders.isCompact, image_add_right, coe_infsep_of_offDiag_nonempty, Set.powersetCard.orderIsoOfFin_apply_coe, mulRothNumber_spec, card_sups_iff, AddSubgroup.rank_closure_finset_le_card, toFinset_coe, SimpleGraph.isClique_map_finset_iff, SimpleGraph.isMaximalIndepSet_compl, biSup_finsetSigma', Module.Basis.reindexFinsetRange_apply, Set.iInter_eq_iInter_finset, SimpleGraph.mem_incidenceFinset, coe_mem, mul_mem_smul_finset_iff, coe_sdiff, PMF.mem_support_ofFinset_iff, Ideal.IsPrime.inf_le', IsLocalizedModule.finsetIntegerMultiple_image, mem_inv_smul_finset_iff, preimage_mul_right_one', pairwise_cons', MeasurableEquiv.coe_IicProdIoc_symm, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, isLUB_sup_id, zero_mem_neg_add_iff, LieIdeal.rootSpan_mem_invtRootSubmodule, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj, Colex.singleton_le_toColex, Polynomial.of_mem_support_derivative, mem_subsetSum_iff, LieAlgebra.Basis.coroot_eq_h', image₂_subset_iff, mem_sub, Set.powersetCard.orderIsoOfFin_symm_apply_val, Turing.TM2.step_supports, ENNReal.tendsto_tsum_compl_atTop_zero, MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder_of_subset, MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure, Fin.attachFin_Icc, Equiv.Finset.disjUnionEquiv_symm_right, IsNoetherian.range_finsetBasis, AddMonoid.exponent_eq_max'_addOrderOf, mem_range_succ_iff, prod_pi_mulSingle, LieSubalgebra.isNonZero_coe_root, exists_le_maximal, Equiv.Perm.mem_range_ofSubtype_iff, min'_mem, exists_le_of_prod_le', Equiv.Finset.union_inl, mem_Iic, Set.union_finset_finite_of_range_finite, Polynomial.rootsExpandEquivRoots_apply, uniqueMul_of_twoUniqueMul, ProbabilityTheory.Kernel.integral_traj_partialTraj', Ideal.span_eq_top_iff_finite, subtype_eq_univ, bddAbove, exists_subset_of_mem_upShadow, ProbabilityTheory.iIndepFun.meas_biInter, DFinsupp.mem_singleton_apply_iff, Subgroup.leftCoset_cover_const_iff_surjOn, covBy_iff_exists_cons, Equiv.Perm.mem_support_cycleOf_iff, MeasureTheory.Measure.map_piSingleton, alternatingGroup.mem_range_ofSubtype_iff, Submodule.span_attach_biUnion, Finsupp.mapDomain_injOn, right_mem_uIcc, RootPairing.GeckConstruction.lie_h_e, Subgroup.leftCoset_cover_filter_FiniteIndex_aux, Disjoint.notMem_of_mem_left_finset, Set.biInter_finsetSigma_univ, UV.sup_sdiff_mem_of_mem_compression_of_notMem, IsPrimitiveRoot.injOn_pow, Convex.helly_theorem', Fin.attachFin_Ico_eq_Ici, Submodule.exists_finiteIndex_of_cover, Function.updateFinset_singleton, TwoUniqueProds.uniqueMul_of_one_lt_card, ProbabilityTheory.iIndepSets_iff, prod_mulIndicator_subset_of_eq_one, wellFoundedOn_bUnion, prod_pi_mulSingle', sum_preimage_of_bij, MeasureTheory.SimpleFunc.preimage_eq_empty_iff, isIrreducible_iff_sInter, subset_div, FiniteDimensional.span_finset, LocallyFiniteOrder.finset_mem_Ioo, DirectedOn.exists_mem_subset_of_finset_subset_biUnion, exists_card_fiber_le_of_card_le_mul, isGLB_inf, sized_slice, Finsupp.sum_ite_eq', all_card_le_biUnion_card_iff_existsInjective', SimpleGraph.IsFiveWheelLike.snd_notMem, coe_offDiag, Nat.mem_divisorsAntidiagonal, Nat.mem_factoredNumbers_iff_forall_le, coe_pair, LocallyFinite.exists_finset_support, Algebra.Presentation.coeffs_relation_subset_coeffs, one_subset, mem_insert_coe, PartitionOfUnity.coe_finsupport, DoubleCoset.iUnion_finset_leftRel_eq_univ_of_leftRel, MeasureTheory.IsSetSemiring.mem_supClosure_iff, PMF.mem_support_ofMultiset_iff, support_of_fiberwise_sum_subset_image, set_biUnion_singleton, AddSubmonoid.mem_closure_iff_exists_finset_subset, RootPairing.EmbeddedG2.indexEquivAllRoots_symm_apply, Dynamics.IsDynCoverOf.nonempty_inter, Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, BoxIntegral.Prepartition.mem_mk, Multiset.mem_sup_map_support_iff, PartitionOfUnity.exists_finset_nhds_support_subset, mem_finsupp_iff, Finsupp.indicator_apply, coe_Icc, pairwiseDisjoint_smul_iff, Ideal.iInf_sup_eq_top, Polynomial.exists_image_comap_of_monic, InfIrred.finset_inf_eq, SimpleGraph.neighborFinset_subset_between_union, IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, card_preimage_eq_sum_card_image_eq, replicate_mem_sym, ProbabilityTheory.Kernel.aestronglyMeasurable_traj, IsDedekindDomain.exists_forall_sub_mem_ideal, DyckWord.equivTreesOfNumNodesEq_symm_apply_coe, Part.coe_toFinset, coe_bipartiteAbove, filter_univ_mem, MvPolynomial.zero_notMem_coeffs, MeasureTheory.Measure.pi_prod_map_IocProdIoc, LinearRecurrence.sol_eq_of_eq_init, MonoidAlgebra.mem_span_support, Equiv.Finset.disjUnionEquiv_inr, ProbabilityTheory.Kernel.iIndepSets.meas_biInter, IsOfFinOrder.mem_powers_iff_mem_range_orderOf, Shatters.subset_iff, Cardinal.mk_compl_finset_of_infinite, SummationFilter.HasSupport.eventually_le_support, DFinsupp.filter_def, Subalgebra.fg_adjoin_finset, one_lt_card_iff, Equiv.Perm.Basis.card_ofPermHom_support, exists_le_minimal, prod_ite_eq', eq_weightedVSubOfPoint_subset_iff_eq_weightedVSubOfPoint_subtype, tprod_subtype', mem_attach, Finpartition.part_eq_empty, LocallyFiniteOrderTop.finset_mem_Ici, IsUltrametricDist.exists_norm_finset_prod_le, map_subtype_subset, UniqueMul.iff_existsUnique, Filter.mem_iInf_finite', injOn_of_card_image_eq, eq_empty_iff_forall_notMem, MonoidHom.noncommPiCoprod_apply, IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty, UniqueProds.uniqueMul_of_nonempty, Polynomial.restriction_zero, MeasureTheory.isProjectiveMeasureFamily_pi, Tuple.graphEquiv₂_apply, vsub_subset_iff, Equiv.Perm.Basis.ofPermHom_apply, sum_erase_attach, Algebra.essFiniteType_cond_iff, coe_orderIsoOfFin_apply, Finpartition.exists_mem, Equiv.Perm.mem_support_iff_mem_support_of_mem_cycleFactorsFinset, attach_affineCombination_coe, GeneralSchauderBasis.proj_apply_basis_mem, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_map, eq_affineCombination_of_mem_affineSpan_image, pow_mem_pow, Finsupp.mem_range_embDomain_iff, covBy_iff_exists_insert, nonempty_coe_sort, coe_mul, isCompact_iff_finite_subcover, Nat.pairwise_coprime_pow_primeFactors_factorization, Polynomial.bUnion_roots_finite, fiber_nonempty_iff_mem_image, exists_ne_map_eq_of_card_image_lt, mk_coe, IsCompact.exists_finite_cover_vadd, Finsupp.coe_neLocus, tendsto_mulIndicator_biUnion_finset, codisjoint_left, Nonempty.exists_cons_eq, Equiv.Perm.mem_support_cycleOf_iff', IsLocalization.finsetIntegerMultiple_image, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, IsCompact.finite_compact_cover, HahnSeries.SummableFamily.smul_support_subset_prod, Polynomial.Chebyshev.strictAntiOn_node, nonempty_def, MeasureTheory.IsSetRing.biInter_mem, exists_mem_image₂, subset_compl_singleton, RootPairing.GeckConstruction.apply_sum_inl_eq_zero_of_mem_span_h, LieAlgebra.IsKilling.instIsCrystallographicSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, Subgroup.FG.biSup_finset, FreeMonoid.mem_symbols, DyckWord.equivTreesOfNumNodesEq_apply_coe, supIndep_iff_pairwiseDisjoint, Module.le_rank_iff_exists_finset, PrimitiveSpectrum.hull_finsetInf, coe_eq_zero, mem_mulSpan, isGreatest_max', Besicovitch.exist_finset_disjoint_balls_large_measure, Submodule.mem_span_iff_exists_finset_subset, max_mem_image_coe, Submodule.mem_span_mul_finite_of_mem_mul, Finsupp.mem_neLocus, Equiv.Finset.disjUnionEquiv_symm_left, IsNonarchimedean.eval_mvPolynomial_le, Ideal.Factors.isScalarTower, Equiv.Perm.OnCycleFactors.mem_range_toPermHom'_iff, Finpartition.bind_parts, mem_Icc, MeasureTheory.IsProjectiveLimit.measure_univ_eq, exists_mem_insert, Algebra.Presentation.coeffs_relation_subset_core, mem_one, Nat.snd_mem_divisors_of_mem_antidiagonal, Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes, coe_inj, GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous, coe_image_subset_range, FirstOrder.Language.Term.realize_restrictVarLeft', AddSubgroup.exists_finiteIndex_of_leftCoset_cover, exists_minimalFor, exists_subset_of_mem_shadow, ProbabilityTheory.Kernel.partialTraj_compProd_traj, MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum, mem_diag, Nonempty.ciSup_mem_image, IsExposed.sInter, Fintype.prod_ite_mem, one_lt_prod_iff_of_one_le, BoxIntegral.unitPartition.mem_admissibleIndex_of_mem_box, Caratheodory.mem_minCardFinsetOfMemConvexHull, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ι_app, Polynomial.rootsExpandPowToRoots_apply, RootPairing.GeckConstruction.trace_toEnd_eq_zero, MeasureTheory.measureReal_biUnion_finset, SimpleGraph.neighborFinset_subset_between_union_compl, Set.powersetCard.mem_coe_iff, singleton_subset_iff, Finpartition.mem_atomise, coe_image, LinearMap.det_eq_det_toMatrix_of_finset, sum_attach, SimpleGraph.mem_finsetWalkLength_iff, vectorSpan_eq_span_vsub_finset_right_ne, exists_finset_linearIndependent_of_le_finrank, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, Nat.one_mem_divisors, continuous_restrict₂, MeasureTheory.IsSetAlgebra.biUnion_mem, one_mem_inv_mul_iff, IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf, MeasureTheory.projectiveFamilyContent_cylinder, SupIndep.independent, Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical, prod_coe_sort, Polynomial.mem_support_iff, FiniteInter.finiteInter_mem, FreeCommRing.exists_finset_support, SimpleGraph.IsMaximumIndepSet.isMaximalIndepSet, UniqueAdd.addHom_preimage, DFinsupp.mk_zero, setOf_mem, Equiv.Perm.support_noncommProd, IsPrimitiveRoot.primitiveRootsPowEquiv_symm_apply_coe, MonovaryOn.sum_mul_comp_perm_eq_sum_mul_iff, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, Nat.bijOn_ofDigits', Preorder.measurable_frestrictLe₂, Preorder.continuous_frestrictLe, MeasureTheory.IsSetAlgebra.biInter_mem, Fintype.sum_ite_mem, iSup_eq_iSup_finset, Submonoid.exists_minimal_closure_eq_top, Cardinal.mk_coe_finset, FixedDetMatrices.reps_entries_le_m', Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne, isNoetherian_adjoin_finset, RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing, HallMarriageTheorem.hall_cond_of_restrict, sup'_eq_csSup_image, image_add_right', SimpleGraph.mem_indepSetFinset_iff, zero_mem_nsmul, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, mem_filterMap, AddMonoid.closure_finset_fg, RootPairing.Base.chainBotCoeff_eq_zero, mem_disjSups, AddGroup.rank_spec, ProbabilityTheory.Kernel.partialTraj_le_def, sub_mem_sub, sup_attach, subset_powersetCard_univ_iff, Finsupp.prod_attach_index, exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul, card_le_one_iff_subsingleton, mem_pimage, mem_sigmaLift, inl_mem_sumLift₂, subset_diffs, Polynomial.coeff_mem_coeffs, finsuppAntidiagEquivSubtype_symm_apply_coe, MvPolynomial.combinatorial_nullstellensatz_exists_eval_nonzero, Set.PairwiseDisjoint.attach, mem_piDiag, Submodule.fg_span_iff_fg_span_finset_subset, exists_lt_card_fiber_of_mul_lt_card_of_maps_to, exists_max_image, Pi.cons_ne, max_mem_insert_bot_image_coe, Group.rank_spec, AddSubmonoid.exists_minimal_closure_eq_top, finsum_mem_finset_eq_sum, Polynomial.derivativeFinsupp_derivative, notMem_sdiff_of_mem_right, notMem_of_lt_min, Set.Finite.subtypeEquivToFinset_apply_coe, MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty, mem_sym2_iff, Finsupp.embDomain_comapDomain, none_mem_insertNone, prod_lt_one_iff_of_le_one, Bornology.isBounded_biUnion_finset, mem_erase_of_ne_of_mem, ProbabilityTheory.Kernel.condDistrib_trajMeasure, range_subset, DirectSum.mk_apply_of_notMem, Finsupp.mapDomain_comapDomain, MeasureTheory.projectiveFamilyContent_congr, ProbabilityTheory.iCondIndepFun.condIndepFun_finset, MulAction.mem_stabilizer_finset, intervalGapsWithin_surjOn, isClosed, Ideal.IsPrime.prod_mem_iff, measurableSet, inf_attach, Bornology.isCobounded_biInter_finset, measurableSet_biInter, Equiv.Perm.support_cycleOf_eq_nil_iff, affineIndependent_iff_indicator_eq_of_affineCombination_eq, mem_finsupp_iff_of_support_subset, prod_apply_dite, SimpleGraph.TripartiteFromTriangles.is3Clique_iff, Order.exists_orderEmbedding_insert, asymptoticCone_biUnion, Algebra.FiniteType.iff_quotient_freeAlgebra, mk_mem_product, swap_mem_antidiagonal, mem_of_min, Equiv.piFinsetUnion_right, sum_fiberwise_eq_sum_filter, mem_sigma, SimpleGraph.isNIndepSet_iff, prod_div_prod_mem_mulSpan, Int.sum_modEq_ite, MeasureTheory.addContent_sUnion, coe_sups, MvPolynomial.mem_supported, coe_Ioc, Affine.Simplex.points_mem_affineSpan_face, LocallyFinite.exists_finset_mulSupport, Finsupp.comapDomain_surjective, SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff, RootPairing.GeckConstruction.span_range_h'_eq_top, Finsupp.comapDomain_mapDomain, coe_Ioo, DependsOn.update, ProbabilityTheory.Kernel.traj_comp_partialTraj, Nonempty.csSup_mem, Finsupp.mk_mem_graph_iff, invMulSubgroup_eq_mul_inv, addRothNumber_spec, alternatingGroup.map_ofSubtype, tendsto_indicator_biUnion_finset, Finsupp.zero_notMem_frange, SimpleGraph.isClique_map_finset_iff_of_nontrivial, Fin.orderIsoTriple_one, Matrix.exp_sum_of_commute, Tuple.self_comp_sort, Finpartition.mem_part_ofSetoid_iff_rel, set_biInter_inter, LinearMap.ker_noncommProd_eq_of_supIndep_ker, ProbabilityTheory.iCondIndepSets_singleton_iff, Equiv.Finset.union_symm_left, Affine.Simplex.range_face_points, ringKrullDim_le_ringKrullDim_quotient_add_card, Equiv.Perm.toList_eq_nil_iff, IicProdIoc_def, Finsupp.mem_toMultiset, SeparatedNhds.of_finset_finset, LocallyFiniteOrderBot.finset_mem_Iio, MvPolynomial.coe_coeffs_map, Equiv.Perm.Basis.ofPermHom_mem_centralizer, TwoUniqueSums.uniqueAdd_of_one_lt_card, Set.Finite.coe_toFinset, MeasureTheory.Measure.pi_prod_map_IicProdIoc, mem_insert, prod_eq_ite, MeasureTheory.measurableCylinders_nat, antidiagonal_subtype_ext_iff, partialSups_eq_sUnion_image, insert_erase_invOn, SimpleGraph.completeEquipartiteGraph_succ_isContained_iff, 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, MeasureTheory.IsSetSemiring.empty_notMem_disjointOfUnion, Submodule.mem_span_set, singleton_subset_coe, Absorbs.biUnion_finset, range_orderEmbOfFin, IntermediateField.exists_finset_of_mem_supr'', SSet.stdSimplex.mem_face_iff, YoungDiagram.isLowerSet, ext_iff, Dynamics.coverEntropy_biUnion_finset, UniqueAdd.subsingleton, ProbabilityTheory.Kernel.measurable_trajFun, Nonempty.coe_sort, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply, 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, ProbabilityTheory.iIndepFun_iff_finset, Finpartition.part_mem, mem_vadd_finset, Finpartition.exists_enumeration, Profinite.NobelingProof.factors_prod_eq_basis_of_ne, Colex.lt_iff_exists_filter_lt, prod_pow_boole, doubling_lt_two, 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, MonoidAlgebra.coeff_comapDomain, UniqueAdd.exists_iff_exists_existsUnique, inf_eq_bot_iff, ProbabilityTheory.Kernel.lintegral_traj, Submodule.mem_span_finset', subset_iff_notMem, iInf_biUnion, Geometry.SimplicialComplex.indep, Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le, add_subset_iff, Finsupp.prod_indicator_index_eq_prod_attach, iSup_eq_iSup_finset', MeasureTheory.instIsProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, Finsupp.prod_eq_zero_iff, ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, Submodule.IsMinimalPrimaryDecomposition.distinct, not_linearIndependent_iffₒₛ, Colex.toColex_le_toColex, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', RootPairing.GeckConstruction.basis_A_eq, mem_range, coe_coeEmb, ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂, Nat.divisors_eq_map_attach_Iic_factorization_prod_pow, Rel.mem_interedges_iff, swap_mem_addAntidiagonal, coe_ssubset, Equiv.Finset.union_symm_right, LieIdeal.restr_eq_iSup_sl2SubmoduleOfRoot, mem_piAntidiag, preimage_compl, add_mem_vadd_finset_iff, mem_image₂, coe_attach, LieAlgebra.IsKilling.instIsRootSystemSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystem, union_mem_sups, continuous_restrict, isProperLinearSet_iff, eventuallyLE_iUnion, iSupIndep_comp_coe_iff_supIndep, filter_eq', mem_image_const_self, sum_dite_eq', LieAlgebra.IsKilling.isSimple_iff_isIrreducible, inv_filter_univ, AddSubgroup.exists_index_le_card_of_leftCoset_cover, MvPolynomial.support_coeff_finSuccEquiv, doubling_lt_golden_ratio, subset_union_elim, IsLowerSet.nonMemberSubfamily, ProbabilityTheory.Kernel.condExp_traj, Polynomial.rootSet_def, Shatters.exists_inter_eq_singleton, Function.Injective.mem_finset_image, Nonempty.csInf_eq_min', MeasureTheory.partialTraj_const, mem_image₂_of_mem, SimpleGraph.IsNClique.isClique, Equiv.Perm.Basis.mem_support_self, Subgroup.exists_index_le_card_of_leftCoset_cover, Equiv.Perm.OnCycleFactors.val_centralizer_smul, preimage_mul_right_one, sum_pow_of_commute, exists_mem_empty_iff, ProbabilityTheory.Kernel.partialTraj_le, Fin.snoc_mem_piFinset_snoc, MeasureTheory.mem_closedCompactCylinders, AffineIndependent.finrank_vectorSpan_image_finset, Subgroup.exists_leftTransversal_of_FiniteIndex, mem_compl, mem_nsmul, AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff, affineCombination_indicator_subset, Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, IsLocalization.map_integerMultiple, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem, RootPairing.GeckConstruction.span_range_h_le_range_diagonal, SimpleGraph.IsClique.finsetMap, SkewMonoidAlgebra.sum_ite_eq', min_mem_image_coe, three_lt_card_iff, Subgroup.rank_closure_finset_le_card, PMF.support_ofMultiset, iInf_eq_iInf_finset, mulIndicator_biUnion_apply, Set.Sized.uvCompression, erase_mem_shadow, pairwiseDisjoint_filter, MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, noncommSum_insert_of_notMem, zero_subset, not_linearIndependent_iffₛ, hasSum_iff_compl, Finpartition.part_nonempty, Nat.mem_primeFactors_of_ne_zero, coe_compl, MonoidAlgebra.exists_finset_adjoin_eq_top, SimpleGraph.IsFiveWheelLike.snd_notMem_left, pairwise_cons, Finpartition.mem_part_self, MeasureTheory.AddContent.sUnion', UV.sup_sdiff_mem_of_mem_compression, cons_swap, centroid_univ, MeasureTheory.IsSetSemiring.diff_eq_sUnion', SimplexCategory.II.castSucc_mem_finset_iff, Filter.mem_iInf_finset, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, ProbabilityTheory.Kernel.partialTraj_succ_self, Set.Finite.toFinset_ssubset, finsum_mem_finset_product', CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map, Fintype.all_card_le_filter_rel_iff_exists_injective, prod_dite_eq, coe_smul_finset, mem_disjiUnion, sum_indicator_subset_of_eq_zero, LieAlgebra.IsKilling.corootForm_rootSystem_eq_killing, Equiv.Perm.mem_support_of_mem_noncommProd_support, mem_neg_vadd_finset_iff, Fintype.complete, SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image, not_addDissociated_iff_exists_disjoint, three_lt_card, infs_self, FractionalIdeal.spanFinset_ne_zero, inl_mem_sumLexLift, rank_span_finset_le, eventually_cofinite_notMem, eq_singleton_iff_unique_mem, sum_pos_iff_of_nonneg, DirectSum.mk_apply_of_mem, biInf_finsetSigma, LieIdeal.mem_rootSet_of_mem_rootSpan, pi_eq_generateFrom, expect_dite_eq', coe_vadd, LieIdeal.rootSet_apply_coroot_eq_zero_of_notMem_rootSet, RootPairing.GeckConstruction.ω_mul_h, mem_ssubsets, ProbabilityTheory.iCondIndepSet_iff, UniqueMul.mulHom_preimage, measurable_updateFinset, Finsupp.mem_support_finset_sum, sum_ite_zero, SmoothPartitionOfUnity.coe_finsupport, DFinsupp.erase_def, diag_mem_sym2_mem_iff, coe_infsep, Fin.attachFin_uIcc, IsProperSemilinearSet.biUnion_finset, mem_powerset, Set.powersetCard.coe_finset, MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset, MeasureTheory.IsSetSemiring.notMem_disjointOfDiff, disjoint_insert_right, sup_mem_sups, Equiv.Perm.zpow_apply_mem_support, isCompact_iff_finite_subfamily_closed, ciInf_mem_image, ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul, exists_orthonormalBasis, RootPairing.GeckConstruction.instIsIrreducible, IntermediateField.exists_finset_of_mem_iSup, MeasureTheory.sum_measure_preimage_singleton, inf_set_eq_iInter, addConvolution_ne_zero, inclusion_exclusion_card_biUnion, SupIndep.le_sup_iff, mem_range_iff_mem_finset_range_of_mod_eq', Topology.CWComplex.mapsTo', Equiv.Perm.Basis.toPermHom_apply_toCentralizer, Colex.toColex_lt_toColex_iff_exists_forall_lt, Polynomial.one_mem_nthRootsFinset, LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule, MeasureTheory.integral_biUnion_eq_sum_powerset, RootPairing.Base.linearIndepOn_root, Set.Sized.compls, exists_nontrivial_relation_sum_zero_of_not_affine_ind, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, mem_convexHull, biInf_finsetSigma', SimpleGraph.mk_mem_interedges_iff, MeasureTheory.instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic, RootPairing.Base.toCoweightBasis_apply, DiscreteQuotient.comp_finsetClopens, mem_union_of_disjoint, mem_powersetCard, SimpleGraph.coe_finsetWalkLength_eq, pairwiseDisjoint_map_sigmaMk, noncommSum_insert_of_notMem', sum_sub_sum_mem_addSpan, noncommSum_cons, iInf_finset_image, DFinsupp.coe_neLocus, mem_addSpan, Module.Basis.mem_span_image, YoungDiagram.mem_cellsOfRowLens, measurable_IicProdIoc, injOn_of_surjOn_of_card_le, BoxIntegral.Prepartition.pairwiseDisjoint, Submodule.mem_span_mul_finite_of_mem_span_mul, MvPolynomial.mem_support_coeff_optionEquivLeft, SkewMonoidAlgebra.mem_support_iff, AddAction.mem_stabilizer_finset', Finpartition.empty_notMem_parts, Measurable.dependsOn_of_piFinset, hasSum, MvPolynomial.mem_supported_vars, codisjoint_right, Seminorm.exists_apply_eq_finset_sup, DFinsupp.notMem_neLocus, Subgroup.finiteIndex_iInf', card_sq_le_card_mul_mulEnergy, Module.Basis.reindexFinsetRange_repr_self, zero_notMem_sub_iff, RootPairing.Base.span_int_root_support, PiNat.cylinder_eq_pi, SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton, MeasureTheory.IsSetSemiring.disjointOfUnion_subset, Equiv.Perm.OnCycleFactors.mem_ker_toPermHom_iff, AddMonoidAlgebra.exists_supDegree_mem_support, Ideal.iSup_iInf_eq_top_iff_pairwise, MvPolynomial.mem_restrictSupport_iff, FreeAbelianGroup.notMem_support_iff, Equiv.Perm.Basis.ofPermHom_support, Multipliable.prod_mul_tprod_subtype_compl, Convex.exists_subset_interior_convexHull_finset_of_isCompact, ProbabilityTheory.iIndepSets.meas_biInter, Multipliable.tprod_finset_bUnion_disjoint, MeasurableEquiv.coe_IicProdIoc, ProbabilityTheory.Kernel.isProjectiveLimit_trajFun, MeasureTheory.IntegrableOn.finset, Equiv.Perm.IsThreeCycle.eq_swap_mul_swap_iff_mem_support, SubMulAction.fg_iff, MeasureTheory.Measure.haar.addIndex_defined, MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff, le_sup_iff, EMetric.pair_reduction, Monoid.closure_finset_fg, Set.toFinset_subset, sum_indicator_subset, pimage_subset, mem_map_mk, coe_neg, exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum, ProbabilityTheory.isProjectiveMeasureFamily_map_restrict, mem_Ioo, Nat.mem_Ioc_succ', Set.definable_biUnion_finset, SimpleGraph.degree_le_between_add, ProbabilityTheory.cond_iInter, Nonempty.csSup_eq_max', Submodule.torsionBySet_isInternal, Submodule.mem_span_finite_of_mem_span, mem_sdiff, sup_preimage_self, Preorder.frestrictLe_apply, Finpartition.nonuniformWitness_mem_nonuniformWitnesses, Prime.dvd_finsuppProd_iff, isClopen_biUnion_finset, SimplexCategory.II.last_mem_finset, biUnion_Iic_disjointed, convexHull_eq, Preorder.frestrictLe₂_apply, MeasureTheory.VectorMeasure.of_biUnion_finset, default_singleton, RootPairing.GeckConstruction.ωConjLieSubmodule_eq_top_iff, finrank_span_finset_le_card, RootPairing.Base.toCoweightBasis_repr_coroot, AntivaryOn.sum_mul_lt_sum_comp_perm_mul_iff, Fin.attachFin_Ico, GradedRing.mem_support_iff, orderEmbOfCardLe_mem, MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion, finprod_mem_finset_product', Set.Finite.subset_toFinset, left_mem_uIcc, TopologicalSpace.CompactOpens.coe_finsetSup, Filter.biInter_finset_mem, card_filter_le_iff, SimpleGraph.IsFiveWheelLike.fst_notMem_right, Fintype.expect_ite_mem, finprod_mem_coe_finset, coe_preimage, Filter.tendsto_finset_preimage_atTop_atTop, sup_inf, DFinsupp.subtypeSupportEqEquiv_symm_apply_coe, exists_mem_eq_sup, prod_attach_univ, ciInf_eq_min'_image, card_mul_iff, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, SimpleGraph.IsNIndepSet.isIndepSet, Multiset.mem_toEnumFinset, roth_3ap_theorem_nat, mem_shadow_iff_insert_mem, isWF_bUnion, AntivaryOn.sum_smul_comp_perm_eq_sum_smul_iff, ProbabilityTheory.Kernel.traj_map_frestrictLe_of_le, mem_Ioi, coe_eraseNone, coe_disjiUnion, Asymptotics.IsBigOWith.sum_congr, isNilpotent_of_finite_tfae, SimpleGraph.swap_mem_interedges_iff, coe_filterMap, SimpleGraph.coe_incidenceFinset, IsCompact.elim_nhds_subcover, List.zipWith_swap_prod_support', MeasureTheory.IsSetSemiring.sUnion_disjointOfDiffUnion_subset, mem_map_equiv, Polynomial.notMem_support_iff, notMem_uIcc_of_gt, MeasureTheory.ae_restrict_biUnion_finset_iff, Equiv.Perm.pairwise_commute_of_mem_zpowers, notMem_empty, mem_vsub, MvPolynomial.coeff_mul_X', mem_primesOverFinset_iff, mem_div, MeasurableSpace.measurableSet_generateFrom_memPartition_iff, image_injOn_powerset_of_injOn, IsPrimitiveRoot.primitiveRootsPowEquivOfCoprime_apply_coe, ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, Equiv.Perm.mem_ofSign, mem_erase, DFinsupp.mem_support_iff, ssubset_iff, AddSubgroup.leftCoset_cover_const_iff_surjOn, min'_lt_max', SimpleGraph.IsMaximumClique.isClique, Polynomial.Chebyshev.isLocalExtr_T_real_iff, SimpleGraph.cliqueFreeOn_of_card_lt, MeasureTheory.Measure.count_apply_finset', Rel.mk_mem_interedges_iff, coe_list_prod, Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff, PMF.support_ofFinset, Set.PairwiseDisjoint.image_finset_of_le, Equiv.Perm.mem_cycleFactorsFinset_conj', FirstOrder.Language.BoundedFormula.realize_restrictFreeVar', YoungDiagram.mk_mem_col_iff, IsPrimitiveRoot.primitiveRootsPowEquiv_apply_coe, eventuallyEq_iUnion, List.mem_foldr_sup_support_iff, Finsupp.mem_rangeIcc_apply_iff, PrimitiveSpectrum.preimage_upperClosure_compl_finset, exists_le_card_fiber_of_mul_le_card_of_maps_to, mem_preimage, prod_dite_of_false, Multiset.toEmbedding_coeEquiv_trans, sum_eq_tsum_indicator, mem_of_max, Profinite.NobelingProof.e_mem_of_eq_true, hasProd_support, Finpartition.mem_bot_iff, Submodule.span_range_natDegree_eq_adjoin, insert_ne_self, Fintype.coe_piFinset, List.pairwise_iff_coe_toFinset_pairwise, Set.indicator_pi_one_apply, Submodule.IsMinimalPrimaryDecomposition.injOn, SimpleGraph.isMaximalClique_compl, image_subset_iff, coe_eq_univ, Equiv.Perm.subtypePerm_apply_pow_of_mem, MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le, AbsolutelyContinuousOnInterval.biUnion_uIoc_subset_of_mem_disjWithin, Sym2.mem_toFinset, UV.compress_mem_compression, Subgroup.exists_finset_card_le_mul, isCompact_biUnion, Nonempty.inf_eq_bot_iff, UniqueFactorizationMonoid.mem_primeFactors, Polynomial.map_restriction, Submodule.sum_mem_biSup, sups_subset_self, right_notMem_Ico, coe_injective, notMem_of_mem_powerset_of_notMem, min_eq_bot, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, coe_covBy_coe, LieIdeal.mem_rootSet, MvPolynomial.coeff_mem_coeffs, Convex.helly_theorem_set, prod_erase_attach, RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra, Finsupp.mk_mem_graph, fold_min_le, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj, restrict_preimage_univ, IsPrimitiveRoot.injOn_pow_mul, PMF.support_uniformOfFinset, SimpleGraph.CliqueFree.mem_of_sup_edge_isNClique, empty_mem_powerset, preimage_neg, FirstOrder.Language.Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset, IsApproximateSubgroup.of_small_tripling, Equiv.Perm.IsCycle.zpowersEquivSupport_apply, Submodule.isPrimary_decomposition_pairwise_ne_radical, SimpleGraph.componentCompl_finite, sum_pow_eq_sum_piAntidiag_of_commute, rel_iSup_prod, WithTop.prod_eq_top_iff, MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset, exists_finset_linearIndependent_of_le_rank, Ideal.Factors.liesOver, Down.mem_compression_of_insert_mem_compression, card_attach, Caratheodory.mem_convexHull_erase, one_mem_pow, IsUltrametricDist.exists_norm_finset_sum_le, isLUB_sup', iInf_union, AddMonoidAlgebra.exists_finset_adjoin_eq_top, MeasureTheory.lintegral_finset, sigmaAntidiagonalEquivProd_symm_apply_snd_coe, sum_boole_nsmul, not_mem_subset, sym_fill_mem, MeasureTheory.StronglyMeasurable.dependsOn_of_piFinset, MvPolynomial.mem_support_finSuccEquiv, Finsupp.mem_support_multiset_sum, Equiv.Perm.OnCycleFactors.cycleType_kerParam_apply_apply, MeasurableSpace.measurableSet_generateFrom_countablePartition_iff, ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicForallTraj, Set.toFinset_ssubset, sup_eq_iSup, some_mem_insertNone, ProbabilityTheory.identDistrib_iff_forall_finset_identDistrib, CompositionAsSet.getLast_mem, subset_set_image_iff, RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall, div_subset_iff, MeasureTheory.ae_restrict_biUnion_finset_eq, coe_infsep_of_offDiag_empty, Submodule.spanRank_toENat_eq_iInf_finset_card, card_sq_le_card_mul_addEnergy, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf, isCountablyCompact_iff_countable_open_cover, exists_card_fiber_lt_of_card_lt_mul, IsCompact.elim_nhds_subcover_nhdsSet, IsCompact.elim_nhdsWithin_subcover, Submodule.subset_span_finite_of_subset_span, Height.mulHeightBound_eq, ProbabilityTheory.iCondIndepSets_iff, univ_eq_attach, mem_toLeft, UniqueAdd.set_subsingleton, RootPairing.GeckConstruction.ωConj_invFun, mem_inv', Ideal.sum_pow_mem_span_pow, Nat.Iio_factorization_prod_pow_injective, Finsupp.finite_vaddAntidiagonal, prod_extend_by_one, zero_mem_zero, centroid_mem_convexHull, Real.geom_mean_lt_arith_mean_weighted_iff_of_pos, ProbabilityTheory.Kernel.integral_traj_partialTraj, Int.existsUnique_mem_box, Profinite.NobelingProof.spanFinBasis.span, MeasureTheory.Measure.restrict_biUnion_finset, Infinite.exists_notMem_finset, mem_insert_of_mem, untrop_sum, coe_nsmul, ProbabilityTheory.iIndep_iff, Equiv.Perm.mem_cycleFactorsFinset_support, 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.Filtration.piFinset_eq_comap_restrict, MeasureTheory.Measure.haar.addIndex_elim, IsCompact.elim_finite_subcover, Fintype.coe_finsetOrderIsoSet, 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, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', UniqueMul.of_card_le_one, diag_mem_sym2_iff, FractionalIdeal.mem_span_mul_finite_of_mem_mul, SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff', Function.updateFinset_univ_apply, MeasureTheory.addContent_biUnion_eq, SimpleGraph.mem_interedges_iff, ssubset_iff_exists_cons_subset, iInf_insert_update, Equiv.Perm.pow_apply_mem_support, AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq, not_mulDissociated_iff_exists_disjoint, Nat.Prime.mem_primeFactors, isLUB_sup, ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, MeasureTheory.IsProjectiveLimit.measure_cylinder, compact_covered_by_add_left_translates, Equiv.Perm.signBijAux_surj, SSet.stdSimplex.obj₀Equiv_symm_mem_face_iff, card_insert_eq_ite, Multiset.mem_sup, prod_coe_sort_eq_attach, AntivaryOn.sum_mul_lt_sum_mul_comp_perm_iff, measurable_updateFinset', sum_extend_by_zero, IntermediateField.isSplittingField_iSup, sum_neg_iff_of_nonpos, IsCountablyCompact.elim_finite_subcover, exists_le_card_fiber_of_nsmul_le_card_of_maps_to, MeasureTheory.sum_measureReal_preimage_singleton, SimpleGraph.mem_neighborFinset, max_eq_top, addConvolution_pos, MonomialOrder.degree_mem_support, prod_attach_eq_prod_dite, Equiv.Perm.isPretransitive_of_isCycle_mem, finsum_mem_finset_product, ringKrullDim_le_ringKrullDim_add_card, smul_mem_smul_finset, SimpleGraph.IsFiveWheelLike.fst_notMem, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_map_app, self_mem_range_succ, equitableOn_iff, subset_vadd, filter_cons, pi_generateFrom_eq, MonoidAlgebra.support_gen_of_gen, Turing.TM2.stmts₁_self, centroidWeightsIndicator_def, Equiv.Perm.OnCycleFactors.coe_toPermHom, IsTopologicalBasis.iInf, sUnion_disjiUnion, HasAntidiagonal.mem_antidiagonal, PointedCone.mem_span_set, card_eq_succ_iff_cons, Equiv.Perm.IsThreeCycle.nodup_iff_mem_support, notMem_of_coe_lt_min, mem_of_mem_inter_right, Tree.mem_treesOfNumNodesEq_numNodes, exists_mem_ne, MeasureTheory.measure_biUnion_finset_le, FreeAddMonoid.mem_symbols, inter_singleton, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, Cardinal.mk_eq_nat_iff_finset, YoungDiagram.mem_col_iff, piFinset_filter_const, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, isPWO_bUnion, List.support_formPerm_le', dependsOn_restrict, coe_symmDiff, mem_sup', CompositionAsSet.zero_mem, Set.ssubset_toFinset, IsCompact.elim_nhds_subcover', isCountablyCompact_biUnion, DFinsupp.mem_pi, inf_sSup_eq_iSup_inf_sup_finset, prod_ite_mem, IsNoetherian.coe_finsetBasisIndex, Nat.prod_pow_primeFactors_factorization, inr_mem_sumLift₂, MonovaryOn.sum_smul_comp_perm_eq_sum_smul_iff, iInf_singleton, Set.iUnion_eq_iUnion_finset, measure_zero, WithTop.sum_eq_top, mem_disjSum, ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj, Finsupp.sum_comapDomain, RootPairing.GeckConstruction.isNilpotent_f, SimpleGraph.mem_cliqueFinset_iff, sum_ite_mem_eq, Finsupp.notMem_graph_snd_zero, Tree.coe_treesOfNumNodesEq, Colex.le_def, SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton, notMem_union, Monoid.exponent_eq_max'_orderOf, pairwiseDisjoint_piAntidiag_map_addRightEmbedding, isOpen_biInter_finset, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, sum_dite_of_false, mem_bipartiteBelow, filter_ssubset, noncommProd_cons', forall_coe, exists_maximal, RootPairing.GeckConstruction.lie_e_f_same, SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, MeasureTheory.Measure.isProjectiveLimit_infinitePiNat, mem_falling, Algebra.FiniteType.iff_quotient_mvPolynomial, coeAddMonoidHom_apply, max'_eq_iff, IsPiSystem.tendsto_probabilityMeasure_biUnion, RootPairing.GeckConstruction.ω_mul_ω, AddSubgroup.FG.biSup_finset, RootPairing.GeckConstruction.f_lie_v_ne, MeasureTheory.Measure.count_apply_finset, Equiv.Perm.perm_inv_on_of_perm_on_finset, MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff, Caratheodory.affineIndependent_minCardFinsetOfMemConvexHull, Nat.prod_modEq_ite, Finpartition.mem_bind, Submodule.mem_span_image_finset_iff_exists_fun, alternatingGroup.range_ofSubtype, DFinsupp.lmk_apply, UV.mem_of_mem_compression, tendsto_tsum_compl_atTop_zero, subset_iff, exists_next_right, mem_of_mem_filter, Module.exists_nontrivial_relation_sum_zero_of_finrank_succ_lt_card, preimage_add_right_singleton, AddMonoidAlgebra.mem_adjoin_support, AffineIndependent.vectorSpan_image_finset_eq_of_le_of_card_eq_finrank_add_one, IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime, linearIndependent_iff_finset_linearIndependent, DependsOn.dependsOn_lmarginalPartialTraj, isPWO, Finsupp.mem_support_single, Equiv.Perm.OnCycleFactors.Subgroup.Centralizer.toConjAct_smul_mem_cycleFactorsFinset, RootPairing.GeckConstruction.ωConj_toFun, bddBelow, Submodule.iSup_torsionBy_eq_torsionBy_prod, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, coe_zero, all_card_le_biUnion_card_iff_exists_injective, mem_inf, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_map_app, Nontrivial.coe, Set.image_finset_sum_pi, SimpleGraph.mk_mem_interedges_comm, mulSupport_prod, RootPairing.GeckConstruction.e_lie_v_ne, PointedCone.DualFG.dual_of_finset, Ideal.sup_iInf_eq_top, isClopen_biInter_finset, coe_diffs, mem_subtype, PiTensorProduct.tprod_noncommProd, mem_zmultiples_iff_mem_range_addOrderOf, Behrend.mem_box, IsCompact.elim_nhdsWithin_subcover', sym_filterNe_mem, Ideal.Factors.finrank_pow_ramificationIdx, AffineIndependent.convexHull_inter', subset_sub, prod_powerset_cons, notMem_of_max_lt_coe, MeasureTheory.Measure.restrict_biUnion_finset_congr, le_max', HallMarriageTheorem.hall_hard_inductive_step_B, RootPairing.GeckConstruction.ω_mul_e, choose_spec, MeasureTheory.SimpleFunc.mem_restrict_range, sup_mem_of_nonempty, List.pairwiseDisjoint_consFixedLengthDigits, SimpleGraph.IsMaximumClique.isMaximalClique, isLUB_mem, RootPairing.GeckConstruction.isNilpotent_e, Dense.diff_finset, noncommProd_mul_distrib_aux, ProbabilityTheory.Kernel.partialTraj_self, sigmaAntidiagonalEquivProd_symm_apply_fst, MonovaryOn.sum_comp_perm_mul_eq_sum_mul_iff, linearIndepOn_finset_iffₛ, exists_of_linearIndepOn_of_finite_span, ProbabilityTheory.Kernel.traj_apply, Finsupp.mem_vaddAntidiagonal_of_addGroup, MeasureTheory.IsProjectiveMeasureFamily.congr_cylinder, Topology.CWComplex.cellFrontier_subset_finite_openCell, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, MeasureTheory.IsSetSemiring.subset_of_diffUnion_disjointOfDiffUnion, iInter_mem_sets, exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul, Seminorm.zero_or_exists_apply_eq_finset_sup, LieAlgebra.Basis.cartanMatrix_base_eq, restrict₂_def, convexHull_eq_union_convexHull_finite_subsets, union_support_maximal_linearIndependent_eq_range_basis, Equiv.Perm.pow_apply_mem_toList_iff_mem_support, Module.FinitePresentation.out, SimplexCategory.II.mem_finset_iff, RootPairing.Base.exists_root_eq_sum_int, Submodule.exists_finset_span_eq_linearIndepOn, Set.definable_biInter_finset, IntermediateField.exists_finset_of_mem_adjoin, one_lt_prod_iff, mem_of_mem_erase, Nonempty.attach, ENNReal.sum_add_tsum_compl, right_mem_Icc, RootPairing.GeckConstruction.h_mem_lieAlgebra, IsUltrametricDist.exists_norm_finset_sum_le_of_nonempty, IicProdIoc_preimage, mem_shadow_iterate_iff_exists_card, coe_Ioi, mem_sumLexLift, Equiv.Perm.subtypePerm_on_cycleFactorsFinset, left_notMem_Ioc, Fin.attachFin_Iio, FirstOrder.Language.distinctConstantsTheory_eq_iUnion, Function.updateFinset_univ, MeasureTheory.addContent_biUnion, PiFinsetCoe.canLift, sized_shadow_iff, SimpleGraph.mem_edgeFinset, Colex.lt_iff_max'_mem, MeasureTheory.IsProjectiveMeasureFamily.measure_univ_eq, FractionalIdeal.spanFinset_coe, MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion, 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, Tree.mem_treesOfNumNodesEq, card_add_iff, FixedPoints.linearIndependent_smul_of_linearIndependent, Colex.erase_le_erase_min', sum_pi_single', DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ, RootPairing.Base.toWeightBasis_apply, MeasureTheory.measure_biUnion_finset₀, Polynomial.coeff_restriction, eq_weightedVSub_subset_iff_eq_weightedVSub_subtype, 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, Set.piCongrLeft_comp_restrict, Summable.tsum_finset_bUnion_disjoint, Topology.RelCWComplex.mapsTo, empty_mem_ssubsets, notMem_Iio_self, MeasureTheory.measure_biUnion_finset, isLowerSet_shatterer, map_noncommProd, TopologicalSpace.Clopens.coe_finset_sup, MvPolynomial.mem_coeffsIn_iff_coeffs_subset, Submodule.mem_iSup_finset_iff_exists_sum, ProbabilityTheory.iCondIndepFun_iff, Finpartition.part_eq_iff_mem, min'_eq_iff, mem_powersetCard_univ, prod_fiberwise_eq_prod_filter', exists_not_mem_of_card_lt_enatCard, coe_eq_one, MvPolynomial.weightedDecomposition.decompose'_eq, sum_pi_single, Polynomial.natTrailingDegree_mem_support_of_nonzero, isGLB_iff_isLeast, pairwiseDisjoint_vadd_iff, TopologicalSpace.exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact, surj_on_of_inj_on_of_card_le, surjOn_of_injOn_of_card_le, Submodule.exists_isInternal_prime_power_torsion, inclusion_exclusion_sum_biUnion, Subgroup.leftCoset_cover_filter_FiniteIndex, 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, Dynamics.netMaxcard_finite_iff, notMem_sigmaLift_of_ne_left, multipliable_compl_iff, LieAlgebra.IsKilling.rootSystem_pairing_apply, preimage_subset, Finpartition.existsUnique_mem, rank_span_of_finset, Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous, IsOfFinAddOrder.multiples_eq_image_range_addOrderOf, pairwise_subtype_iff_pairwise_finset', Nat.mem_primeFactors_iff_mem_primeFactorsList, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff, mem_smul_finset, BoxIntegral.unitPartition.mem_prepartition_iff, disjiUnion_map, exists_ne_one_of_prod_ne_one, MvPolynomial.exists_finset_rename₂, disjoint_insert_left, infsep_zero_iff_subsingleton, exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul, support_prod_subset, SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle, DFinsupp.mk_add, OrthonormalBasis.span_apply, Nat.self_notMem_properDivisors, mem_pi, image_preimage_of_bij, mem_upShadow_iff_exists_sdiff, filter_inj, AddMonoidAlgebra.support_divOf, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, convexIndependent_iff_finset, preimage_inv, card_eq_succ, Equiv.Perm.ofSubtype_eq_iff, prod_indicator, Finsupp.sum_attach_index, iSup_insert_update, BoxIntegral.Prepartition.iUnion_def', RootPairing.EmbeddedG2.indexEquivAllRoots_apply_coe, exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to, Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Group.fg_iff', Set.iInter_eq_iInter_finset', card_image_iff, 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, Set.encard_coe_eq_coe_finsetCard, MvPolynomial.mem_vars_rename, Fin.cons_mem_piFinset_cons, Filter.iInf_sets_eq_finite, subset_set_image₂, MeasureTheory.measurePreserving_piFinsetUnion, Equiv.Perm.IsCycle.zpowersEquivSupport_symm_apply, notMem_range_self, mem_disjUnion, notMem_of_max_lt, instIsEmpty, DFinsupp.mem_rangeIcc_apply_iff, ProbabilityTheory.Kernel.integrable_traj, coe_pimage, SimpleGraph.isMaximumIndepSet_iff, Submodule.mem_span_image_finset_iff_exists_fun', MeasureTheory.sum_measure_singleton, UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime, SimpleGraph.end_hom_mk_of_mk, subtype_eq_empty, Finsupp.prod_ite_eq, Submonoid.mem_closure_finset, MeasureTheory.dependsOn_cylinder_indicator_const, Shatters.exists_superset, ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq, mem_add, Equiv.Perm.mem_cycleFactorsFinset_iff, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff, mem_of_mem_insert_of_ne, coe_div, LieAlgebra.IsKilling.rootSpace_zsmul_add_ne_bot_iff_mem, Geometry.SimplicialComplex.face_subset_face_iff, exists_lt_of_expect_lt, isSemilinearSet_iff, Submodule.isInternal_prime_power_torsion, Tuple.eq_sort_iff', ProbabilityTheory.Kernel.traj_map_frestrictLe, prod_indicator_const, Multiset.mulSupport_fun_pow_count_subset, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app, mem_inf', coe_Iio, coe_finsetBasisOfLinearIndependentOfCardEqFinrank, shatterer_eq, Int.neg_mem_divisorsAntidiag, mem_compls, inter_insert, image_insert_memberSubfamily, Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one, convolution_eq_zero, prod_dite, SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff, Set.instCanLiftFinsetCoeFinite, ProbabilityTheory.Kernel.integral_traj, sup_eq_sSup_image, preimage_mul_left_one', AddAction.stabilizer_coe_finset, Equiv.restrictPreimageFinset_apply_coe, restrict_preimage, Turing.PartrecToTM2.trStmts₁_self, RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff, RootPairing.GeckConstruction.lie_h_f, image_add_left', ProbabilityTheory.Kernel.traj_map_frestrictLe_apply, Ideal.isCoprime_biInf, isGLB_mem, RootPairing.GeckConstruction.ω_mul_f, UniqueSums.uniqueAdd_of_nonempty, ConvexOn.le_sup_of_mem_convexHull, sub_subset_iff, ProbabilityTheory.isProjectiveLimit_map, WithTop.top_mem_insertTop, Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq, exists_min_image, Int.mem_box, SimpleGraph.exists_of_maximal_cliqueFree_not_adj, ENat.sum_eq_top, Nontrivial.exists_ne, MeasureTheory.IsSetRing.biUnion_mem, BoxIntegral.Prepartition.mem_ofWithBot, 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.Basis.ofPermHomFun_apply_of_cycleOf_mem, Subspace.top_mem_of_biUnion_eq_univ, ProbabilityTheory.uniformOn_apply_finset', Equiv.Perm.OnCycleFactors.toPermHom_apply, card_mul_finset_lt_two, exists_mem_eq_sup', SkewMonoidAlgebra.notMem_support_iff, Group.closure_finset_fg, Finsupp.restrictSupportEquiv_symm_single, coe_product, SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff', mul_subset_iff, MeasureTheory.Measure.infinitePi_cylinder, MeasureTheory.closedCompactCylinders.isClosed, card_infs_iff, MeasureTheory.projectiveFamilyFun_congr, attach_affineCombination_of_injective, prod_ite_mem_eq, disjoint_right, exists_compls_iff, AddSubmonoid.FG.exists_minimal_closure_eq, MvPolynomial.support_divMonomial, Fin.mem_piFinset_iff_last_init, CompositionAsSet.mem_boundaries_iff_exists_blocks_sum_take_eq, sup'_id_eq_csSup, coe_sym2, RootPairing.Base.toWeightBasis_repr_root, RootPairing.GeckConstruction.ωConj_mem_of_mem, Preorder.measurable_frestrictLe, Set.iUnion_finset_eq_set, MeasureTheory.addContent_sUnion_le_sum, Polynomial.degreeLT_eq_span_X_pow, one_notMem_inv_mul_iff, coe_compls, lt_sup_iff, Finpartition.mk_mem_sparsePairs, Finpartition.IsEquipartition.exists_partsEquiv, Function.updateFinset_def, mem_smulAntidiagonal, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_π_app, PolynomialLaw.range_φ, List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint, MeasureTheory.partialTraj_const_restrict₂, supIndep_attach, Module.Basis.repr_support_subset_of_mem_span, attach_val, Finsupp.supportedEquivFinsupp_apply_support_val, UniqueMul.set_subsingleton, coe_inv, RootPairing.Base.coroot_mem_or_neg_mem, RootPairing.GeckConstruction.lie_e_lie_f_apply, Nat.sum_modEq_ite, mem_inv, inf'_le_iff, Equiv.Perm.mem_finPairsLT, MeasureTheory.Filtration.piLE_eq_comap_frestrictLe, MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated, Finsupp.mem_vaddAntidiagonal_iff, Equiv.Perm.subtypePerm_apply_zpow_of_mem, SupIndep.pairwiseDisjoint, DFinsupp.mk_apply, symInsertEquiv_apply_snd_coe, countable_toSet, sigma_preimage_mk_of_subset, iSup_finset_image, subset_erase, AntivaryOn.sum_comp_perm_mul_eq_sum_mul_iff, Finsupp.mem_support_onFinset, exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum, invMulSubgroup_eq_inv_mul, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn, measurable_restrict_apply, mem_perms_of_finset_iff, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, sups_subset_iff, Nat.fst_mem_divisors_of_mem_antidiagonal, CompleteLattice.IsCompactElement.exists_finset_of_le_iSup, YoungDiagram.exists_notMem_col, Affine.Simplex.ExcenterExists.signedInfDist_excenter, linearIndepOn_iff_linearIndepOn_finset, SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff, MvPolynomial.mem_support_coeff_finSuccEquiv, Turing.TM1.stmts₁_self, mem_upShadow_iff_erase_mem, SimpleGraph.completeBipartiteGraph_isContained_iff, AddGroup.closure_finset_fg, one_notMem_div_iff, xInTermsOfW_vars_aux, map_noncommSum, neg_mem_neg, Turing.TM1.stmts_trans, mem_offDiag, MonoidAlgebra.mem_supported, mem_filter, inf_eq_sInf_image, Directed.exists_mem_subset_of_finset_subset_biUnion, ProbabilityTheory.Kernel.map_traj_succ_self, Colex.toColex_lt_toColex, Nonempty.to_subtype, inf_eq_iInf, Polynomial.isRoot_prod, SimpleGraph.isNClique_iff, not_linearIndepOn_finset_iff, SimpleGraph.mem_finsetWalkLengthLT_iff, ProbabilityTheory.iIndepSet_iff_meas_biInter, Multiset.coeEquiv_symm_apply_fst, two_lt_card, card_image₂_iff, LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, mem_upShadow_iff_exists_mem_card_add_one, Cardinal.mk_set_eq_nat_iff_finset, set_biUnion_union, prod_indicator_const_apply, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, mem_union, Submodule.CoFG.sInf, Finsupp.restrictSupportEquiv_apply, mem_map', expect_dite_eq, FiniteDimensional.exists_is_basis_integral, Equiv.Finset.disjUnionEquiv_inl, RootPairing.GeckConstruction.f_lie_v_same, MonomialOrder.notMem_support_of_degree_lt, Turing.TM2.stmts_trans, not_linearIndependent_iff, mem_smul, exists_notMem, MonovaryOn.sum_comp_perm_smul_eq_sum_smul_iff, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset, Equiv.Perm.Basis.ofPermHomFun_mul, sups_eq_self, mem_toRight, mem_inter_of_mem, PairReduction.point_mem_finset_logSizeBallSeq, IsNonarchimedean.apply_sum_le, PMF.uniformOfFinset_apply, Set.exists_finite_iff_finset, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj, inf'_id_eq_csInf, isConnected_iff_sUnion_disjoint_open, Polynomial.natDegree_mem_support_of_nonzero, hasProd_compl_iff, disjoint_singleton_right, sSupIndep_iff_finite, coe_filter_univ, ConvexOn.exists_ge_of_centerMass, Nontrivial.exists_cons_eq, Polynomial.natDegree_restriction, Finmap.mem_keys, UniqueAdd.of_card_le_one, div_mem_div, powerset_card_disjiUnion, UV.compress_disjoint, ClassGroup.finsetApprox.zero_notMem, inv_smul_mem_iff₀, noncommProd_insert_of_notMem', add_mem_add, mem_symmDiff, singleton_inter, not_subset, Equiv.Finset.union_inr, nodup_map_iff_injOn, IsOfFinOrder.powers_eq_image_range_orderOf, prod_attach, ProbabilityTheory.map_restrict_eq_of_forall_ae_eq, Caratheodory.minCardFinsetOfMemConvexHull_subseteq, Multiset.mem_sum, set_biUnion_option_toFinset, HallMarriageTheorem.hall_hard_inductive_step_A, SimpleGraph.Coloring.surjOn_of_card_le_isClique, filter_cons_of_pos, hasProd_prod_disjoint, isGLB_inf_id, map_subset_iff_subset_preimage, disjoint_singleton_left, Subgroup.exists_finiteIndex_of_leftCoset_cover_aux, vadd_stabilizer_of_no_doubling, sum_apply_dite, symInsertEquiv_apply_fst, Profinite.NobelingProof.eval_eq_πJ, isAddUnit_coe, Metric.AreSeparated.finset_iUnion_left, coe_zpow, AffineIndependent.exists_affineCombination_eq_smul_eq, MeasureTheory.Measure.haar.index_defined, Finpartition.parts_top_subsingleton, restrict_def, Polynomial.Monic.irreducible_iff_natDegree', SimpleGraph.degree_le_between_add_compl, diffs_subset_iff, Ideal.Factors.finiteDimensional_quotient_pow, Submodule.mem_iSup_iff_exists_finset, finite_toSet, mem_uIcc_of_ge, Dynamics.coverMincard_finite_iff, hasProd, Nat.mem_factoredNumbers, sum_attach_univ, mem_diffs, Nat.mem_divisors_prime_pow, AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux, convexHull_eq_union, IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element, RootPairing.Base.span_root_support, AddAction.mem_stabilizer_finset, Numbering.mem_prefixed, PiFinsetCoe.canLift', GeneralSchauderBasis.range_proj_eq_span, Ideal.eq_inf_of_isPrime_inf, untrop_sum_eq_sInf_image, AddMonoidAlgebra.support_gen_of_gen, Fintype.card_filter_piFinset_const, LinearMap.coe_det, mem_slice, Nat.mem_smoothNumbersUpTo, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff, 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, Equiv.Perm.exists_mem_support_of_mem_support_prod, LocallyFiniteOrder.finset_mem_Ioc, sized_falling, prod_sum, op_smul_stabilizer_of_no_doubling, Submodule.mem_sSup_iff_exists_finset, Submonoid.mem_closure_finset', mem_memberSubfamily, Colex.le_iff_sdiff_subset_lowerClosure, finsuppAntidiag_insert, mem_image₂_iff, MeasureTheory.measureReal_biUnion_finset_le, PairReduction.point_logSizeBallSeq_add_one, AddMonoidAlgebra.mem_span_support', MeasureTheory.Measure.infinitePi_map_restrict, mem_inv_smul_finset_iff₀, LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdeal, ProbabilityTheory.Kernel.iIndepFun.meas_biInter, Polynomial.mem_coeffs_iff, Equiv.Perm.eq_cycleOf_of_mem_cycleFactorsFinset_iff, SmoothPartitionOfUnity.mem_fintsupport_iff, Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff, Equiv.Perm.Basis.cycleOf_eq, not_linearIndepOn_finset_iffₛ, inf'_eq_csInf_image, Set.iUnion_eq_iUnion_finset', Ideal.subset_union_prime, Module.Finite.span_finset, mem_Ioc, Ideal.prod_eq_iInf_of_pairwise_isCoprime, prod_dite_eq', MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_mem, exists_pos_of_sum_zero_of_exists_nonzero, mem_neg, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer, LieAlgebra.Basis.root_mem_or_mem_neg, Nonempty.one_mem_div, tprod_subtype, Profinite.NobelingProof.one_sub_e_mem_of_false, Finpartition.bot_notMem, Equiv.Perm.two_le_length_toList_iff_mem_support, nullMeasurableSet, Equiv.Perm.signBijAux_mem, DirectSum.support_subset, Nonempty.csInf_mem, Fin.mem_piFinset_iff_zero_tail, notMem_mono, Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow, notMem_erase, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂, exists_eq_insert_iff, IsCompact.elim_nhds_subcover_nhdsSet', two_lt_card_iff, Int.swap_mem_divisorsAntidiag, prod_indicator_biUnion_sub_indicator, coe_map, mem_multiples_iff_mem_range_addOrderOf, YoungDiagram.mem_mk, Set.biUnion_finsetSigma', Finsupp.mem_support_toFun, Nat.mem_properDivisors, symInsertEquiv_symm_apply_coe, notMem_uIcc_of_lt, algebraicIndependent_finset_map_embedding_subtype, MeasureTheory.setIntegral_finset, MvPowerSeries.coeff_truncFinset, mem_Iio, measurable_IocProdIoc, HallMarriageTheorem.hall_cond_of_compl, MeasureTheory.measureReal_biUnion_finset₀, disjoint_left, Ideal.exist_integer_multiples_notMem, prod_mulIndicator_eq_prod_inter, Polynomial.coeff_restriction', Ideal.Factors.isPrime, Equiv.piFinsetUnion_left, Equiv.Perm.IsCycle.commute_iff, List.support_formPerm_of_nodup', PrimeSpectrum.exists_image_comap_of_finite_of_free, set_biInter_singleton, noncommSum_cons', Behrend.threeAPFree_image_sphere, DFinsupp.mk_sub, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, Finsupp.mem_graph_iff, sum_dite_of_true, Set.mem_toFinset, linearIndependent_finset_map_embedding_subtype, vadd_mem_vadd_finset_iff, coe_add, Equiv.Perm.pairwise_disjoint_of_mem_zpowers, Turing.TM1to0.tr_supports, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, preimage_map, Ideal.isPrimary_decomposition_pairwise_ne_radical, lt_fold_max, Nat.sigmaAntidiagonalTupleEquivTuple_apply, ProbabilityTheory.Kernel.iIndepSets_singleton_iff, PairReduction.point_logSizeBallSeq_zero, WCovBy.finset_coe, ClassGroup.mem_finsetApprox, FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem, AddSubgroup.exists_leftTransversal_of_FiniteIndex, Finsupp.support_subset_iff, coe_Ici, mem_map, intervalGapsWithin_mapsTo, RingHom.locally_iff_finite, ENat.exists_le_of_sum_le, mulIndicator_biUnion_finset_eventuallyEq, MeasureTheory.integral_restrict_infinitePi, mulSupport_of_fiberwise_prod_subset_image, addDissociated_iff_sum_eq_subsingleton, EuclideanSpace.restrict₂_apply, mem_infs, IsLocalizedModule.smul_mem_finsetIntegerMultiple_span, ProbabilityTheory.Kernel.iIndepSets.piiUnionInter_of_notMem, Equiv.Perm.CycleType.count_def, ENNReal.sum_eq_top, exists_sum_eq_one_iff_pairwise_coprime, MeasureTheory.addContent_biUnion_le, YoungDiagram.mk_mem_row_iff, SimpleGraph.Walk.coe_edges_toFinset, coe_notMemRangeEquiv_symm, Fintype.sum_extend_by_zero, covBy_iff_exists_erase, Seminorm.ball_finset_sup_eq_iInter, Fintype.piFinset_subsingleton, Polynomial.support_restriction, Submodule.finset_span_isCompactElement, SimpleGraph.card_toFinset_mem_edgeFinset, partialSups_eq_biUnion_range, isClosed_biUnion_finset, Polynomial.rootSet_prod, WithTop.prod_eq_top_ex_top, wellFoundedOn, FreeAbelianGroup.mem_support_iff, mem_union_right, ProbabilityTheory.Kernel.lintegral_traj₀, mem_union_left, subset_vsub, Ideal.IsPrime.prod_mem_iff_exists_mem, Affine.Simplex.exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter, erase_eq_self, RootPairing.Base.cartanMatrixIn_mul_diagonal_eq, mem_shadow_iff, pi_eq_empty, preimage_add_left_zero', pairwise_isRelPrime_iff_isRelPrime_prod, Submodule.mem_span_set_iff_exists_finsupp_le_finrank, CovBy.finset_coe, mem_image_of_mem, finprod_mem_finset_product₃, neg_vadd_mem_iff, mem_inter, Down.erase_mem_compression_of_mem_compression, nontrivial_def, BoxIntegral.Prepartition.iUnion_ofWithBot, PMF.toOuterMeasure_apply_finset, restrict_comp_piCongrLeft, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum, subset_smul, PartitionOfUnity.mem_fintsupport_iff, LocallyFinite.exists_finset_nhds_mulSupport_subset, choose_mem, RootPairing.GeckConstruction.f_mem_lieAlgebra, MeasureTheory.integral_finset, Option.mem_toFinset, NNReal.tendsto_tsum_compl_atTop_zero, isTopologicalBasis_pi, RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos, mem_shadow_iterate_iff_exists_mem_card_add, Nat.mem_primesBelow, Set.Intersecting.exists_mem_finset, Set.PairwiseDisjoint.biUnion_finset, Fin.orderIsoTriple_two, Multiset.coeEquiv_symm_apply_snd_val, finprod_mem_finset_eq_prod, inf'_le_of_le, filter_attach, coe_zsmul, DFinsupp.eq_mk_support, Ico_subset_biUnion_Ico, Convex.helly_theorem_set', fiber_card_ne_zero_iff_mem_image, Set.Finite.exists_finset_coe, sum_fiberwise_eq_sum_filter', Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset, forall_mem_not_eq', IsLocalizedModule.map_integerMultiple, Module.Basis.reindexFinsetRange_repr, Finsupp.mem_frange, Submodule.torsionBy_isInternal, coe_inter, Submodule.mem_set_smul, ProbabilityTheory.iIndepFun.restrict, Metric.AreSeparated.finset_iUnion_right, attach_map_val, Nonempty.ciSup_eq_max'_image, le_rank_iff_exists_linearIndependent_finset, attach_empty, SupPrime.le_finset_sup, MeasureTheory.measureReal_biUnion_eq_sum_powerset, CovBy.exists_finset_cons, RootPairing.GeckConstruction.e_mem_lieAlgebra, Units.mk0_prod, Set.Finite.exists_finset, preimage_add_right_zero, IsDedekindDomain.exists_representative_mod_finset, ProbabilityTheory.Kernel.iIndepFun.indepFun_finset₀, MeasureTheory.SimpleFunc.mem_range_self, mem_toList, infs_self_subset, MeasureTheory.SimpleFunc.support_eq, set_biUnion_preimage_singleton, Multiset.support_fun_nsmul_count_subset, exists_lt_of_sum_lt, iSup_option_toFinset, RootPairing.GeckConstruction.lie_h_h, Nat.Prime.mem_primeFactors', Finsupp.comapDomain_add_of_injective, MeasureTheory.squareCylinders_eq_iUnion_image, isGLB_inf', filter_attach', IsLocalization.ideal_eq_iInf_comap_map_away, convolution_pos, RootPairing.GeckConstruction.linearIndependent_h, sum_powerset_cons, Nonempty.to_set, Topology.CWComplex.mapsTo, mem_upShadow_iff, Submonoid.FG.biSup_finset, MultilinearMap.map_sub_map_piecewise, exists_signed_sum, rado_selection_subtype, IsNonarchimedean.finset_powerset_image_add, smul_subset_iff, mem_map_of_mem, coe_insert, finsum_mem_finset_product₃, subset_coe_filter_of_subset_forall, Matroid.Indep.augment_finset, mem_shadow_iff_exists_mem_card_add_one, Algebra.essFiniteType_iff, card_diffs_iff, UV.mem_compression, mem_finsuppAntidiag', Algebra.EssFiniteType.cond, exists_maximalFor, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, sum_coe_sort_eq_attach, SimpleGraph.IsFiveWheelLike.notMem_right, insert_mem_upShadow, WithTop.some_mem_insertTop, sdiff_mem_diffs, weightedVSub_indicator_subset, set_biInter_option_toFinset, indicator_biUnion_eq_sum_powerset, mem_bipartiteAbove, ConvexOn.inf_le_of_mem_convexHull, Set.biUnion_finsetSigma_univ', GradedAlgebra.mem_support_iff, PartitionOfUnity.exists_finset_nhds', mem_cons, NormedSpace.exp_sum_of_commute, Equiv.Perm.mem_conj_support, finsuppAntidiagEquiv_symm_apply_apply, RootPairing.EmbeddedG2.allRoots_subset_range_root, exists_lt_of_prod_lt', SimpleGraph.componentComplFunctor_map, PointedCone.mem_hull_set, AddSubgroup.finiteIndex_iInf', vadd_mem_vadd_finset, lcm_eq_zero_iff, Polynomial.degreeLE_eq_span_X_pow, AddSubmonoid.mem_closure_finset', Finpartition.IsEquipartition.exists_partPreservingEquiv, LieAlgebra.Basis.coe_linearMap_baseSupp', LocallyFiniteOrderTop.finset_mem_Ioi, ProbabilityTheory.Kernel.lmarginalPartialTraj_succ, piiUnionInter_singleton_left, exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum, MvPolynomial.mem_vars_bind₁, Rel.swap_mem_interedges_iff, Nat.mem_divisors_self, SimpleGraph.coe_finsetWalkLengthLT_eq, Int.prod_modEq_ite, MvPolynomial.mem_coeffs_iff, le_sup', ProbabilityTheory.Kernel.iIndepFun.cond_iInter, IsCompact.elim_finite_subfamily_closed, set_biUnion_insert, RootPairing.Base.abs_cartanMatrix_apply, mem_neg', MeasureTheory.IsSetSemiring.exists_finpartition_diff, SimpleGraph.IsMaximumIndepSet.isIndepSet, Finsupp.support_indicator_subset, iInf_option_toFinset, MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset, MeasureTheory.SimpleFunc.map_preimage, SimpleGraph.coe_neighborFinset, partiallyWellOrderedOn_bUnion, zero_mem_smul_iff, LinearMap.diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne, CompactSpace.elim_nhds_subcover, filter_mem_eq_inter, Orthonormal.exists_orthonormalBasis_extension, coe_smul, Preorder.piCongrLeft_comp_restrictLe, pairwiseDisjoint_pair_insert, PairReduction.iSup_edist_pairSet, Equiv.Perm.isInvariant_of_support_le, sum_dite_eq, LocallyFiniteOrderBot.finset_mem_Iic, not_linearIndepOn_finset_iffₒₛ, MvPolynomial.killCompl_monomial, Equiv.Perm.OnCycleFactors.kerParam_range_eq, measurable_restrict₂_apply, RootPairing.GeckConstruction.h_eq_diagonal, mem_product, orderEmbOfFin_mem, exists_of_ssubset, sum_finset_coe, gcd_ne_zero_iff, coe_list_sum, MeasureTheory.measurableCylinders.measurableSet, discreteTopology_biUnion_finset, RootPairing.Base.span_int_coroot_support, IsNoetherian.coeSort_finsetBasisIndex, preimage_mul_right_singleton, exists_coe, isRoot_of_unity_iff, MeasureTheory.IsSetSemiring.subset_disjointOfDiff, SkewMonoidAlgebra.mem_span_support, mem_cons_self, tsum_subtype, Subgroup.exists_finiteIndex_of_leftCoset_cover, apply_union_le_sum, MeasureTheory.mem_measurableCylinders, Fintype.card_coe, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset_obj_obj, expect_ite_eq, exists_ne_zero_of_expect_ne_zero, Nat.notMem_primesBelow, Ideal.Factors.piQuotientEquiv_mk, AffineIndependent.convexHull_inter, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_obj, ProbabilityTheory.Kernel.partialTraj_zero, SeparatedNhds.of_singleton_finset, UniqueMul.subsingleton, hasSum_compl_iff, support_sum, image_mul_right', Set.Finite.subtypeEquivToFinset_symm_apply_coe, FormalMultilinearSeries.mem_compPartialSumTarget_iff, Set.Sized.shadow, sup_id_eq_sSup, one_lt_card, sum_mul_boole, zero_notMem_neg_add_iff, SimpleGraph.edgeFinset_deleteEdges, AddSubgroup.leftCoset_cover_filter_FiniteIndex, IsCompact.elim_finite_subfamily_isClosed_subtype, 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, Set.MapsTo.exists_equiv_extend_of_card_eq, UV.compress_mem_compression_of_mem_compression, singleton_iff_unique_mem, ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, coe_pow, image_add_left, Equiv.Perm.Basis.ofPermHomFun_one, Nat.prodMk_mem_divisorsAntidiag, OrderIso.finsetSetFinite_apply_coe, RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_u, MulAction.mem_stabilizer_finset', SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint, Equiv.Perm.support_subtypePerm, infs_subset_iff, LieAlgebra.Basis.coe_baseSupportEquiv_apply, Finsupp.mem_sym2_support_of_mul_ne_zero, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, subset_infs, Nat.mod_injOn_Ico, coe_vsub, tendsto_tprod_compl_atTop_one, Nat.mem_Ioc_succ, sum_coe_sort, preimage_add_right_zero', Nat.mem_primeFactors, ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_traj, mem_eraseNone, measurableSet_biUnion, Finsupp.mem_splitSupport_iff_nonzero, ciSup_mem_image, IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, mem_attachFin, mem_upShadow_iterate_iff_exists_sdiff, mem_dfinsupp_iff, exists_lt_of_lt_expect, Module.Basis.reindexFinsetRange_self, apply_coe_mem_map, Part.mem_toFinset, Multiset.mem_toFinset, Dynamics.exists_isDynCoverOf_of_isCompact_invariant, Finsupp.notMem_neLocus, Fintype.not_linearIndependent_iffₒₛ, IsDedekindDomain.quotientEquivPiFactors_mk, Preorder.piCongrLeft_comp_frestrictLe, erase_ne_self, mem_powerset_self, MvPolynomial.coeff_add_pow, ProbabilityTheory.Kernel.setIntegral_traj_partialTraj', coe_sum, PMF.mem_support_uniformOfFinset_iff, sup_id_set_eq_sUnion, coe_image₂, Behrend.exists_large_sphere_aux, mem_biUnion, LinearMap.le_rank_iff_exists_linearIndependent_finset, noncommProd_insert_of_notMem, Disjoint.notMem_of_mem_right_finset, Finsupp.prod_ite_eq', Finpartition.exists_le_of_le, IntermediateField.finiteDimensional_iSup_of_finset', inf_mem_infs, AlgebraicGeometry.Scheme.exists_isOpenCover_and_isAffine, DFinsupp.support_subset_iff, mem_sups, 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, sum_ite_eq, eventually_cocardinal_notMem, Equiv.Perm.OnCycleFactors.kerParam_apply, MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset, LieIdeal.root_apply_eq_zero_of_notMem_rootSet, disjiUnion_cons, Down.mem_compression, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff, Prime.dvd_finset_prod_iff, Set.sized_powersetCard, disjiUnion_Iic_disjointed, UniqueAdd.iff_existsUnique, Nat.antidiagonalEquivFin_apply_val, expect_ite_eq', exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul, mem_generatePiSystem_iUnion_elim', Finpartition.not_isEquipartition, sum_eq_ite, Cardinal.finset_card_lt_aleph0, AddMonoidAlgebra.mem_gradeBy_iff, trop_sInf_image, cons_subset, Matroid.IsRkFinite.exists_finset_isBasis', Submonoid.mem_closure_iff_exists_finset_subset, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Set.Intersecting.exists_card_eq, SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff, DFinsupp.mk_smul, Tuple.proj_equiv₁', hasProd_iff_compl, notMem_map_subtype_of_not_property, preimage_inl, MvPolynomial.supported_eq_vars_subset, Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range, Behrend.threeAPFree_sphere, RootPairing.GeckConstruction.apply_inr_eq_zero_of_mem_span_range_u, powersetCard_empty_subsingleton, mem_val, DoubleCoset.iUnion_finset_rightRel_eq_univ_of_rightRel, attach_image_val, LieAlgebra.IsKilling.rootSystem_root_apply, exists_cycleOn, set_biInter_biUnion, support_prod, mem_addAntidiagonal, WithBot.some_mem_insertBot, Profinite.NobelingProof.factors_prod_eq_basis, mem_def, Set.ncard_coe_finset, sup_preimage_val_id, AddMonoidAlgebra.mem_span_support, Metric.AreSeparated.finset_iUnion_left_iff, Down.erase_mem_compression, SimpleGraph.componentCompl_nonempty_of_infinite, LieAlgebra.IsKilling.lieIdeal_eq_inf_cartan_sup_biSup_rootSpace, biUnion_Ioc_disjointed_of_monotone, Seminorm.closedBall_finset_sup_eq_iInter, compact_covered_by_mul_left_translates, WithBot.bot_mem_insertBot, coe_subset_singleton, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion, sum_eq_sum_extend, SubAddAction.fg_iff, MonovaryOn.sum_mul_comp_perm_lt_sum_mul_iff, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, Subgroup.closure_mul_image_eq_top', sigmaAntidiagonalEquivProd_apply, exists_mem_eq_inf', prod_fiberwise_eq_prod_filter, smul_stabilizer_of_no_doubling, Finpartition.part_surjOn, Finpartition.exists_subset_part_bijOn, FirstOrder.Language.Term.realize_restrictVar', filter_eq, FormalMultilinearSeries.mem_compPartialSumSource_iff, zero_mem_box, exists_le_of_sum_le, sigmaAntidiagonalEquivProd_symm_apply_fst, MeasureTheory.Measure.sum_coe_finset, Equiv.Perm.cycleOf_ne_one_iff_mem_cycleFactorsFinset, instNonemptyElemCoeInsert, mul_mem_mul, RootPairing.GeckConstruction.e_lie_u, AddMonoidAlgebra.supDegree_mem_support, Equiv.Perm.zpow_eq_ofSubtype_subtypePerm_iff, image_mul_left, Fin.orderIsoPair_one, Equiv.Perm.OnCycleFactors.range_toPermHom_eq_range_toPermHom', MeasureTheory.isProjectiveLimit_nat_iff', Nat.Iic_factorization_prod_pow_injective, IntermediateField.induction_on_adjoin_finset, Finsupp.mem_pi, Convex.helly_theorem, RootPairing.GeckConstruction.lie_e_f_ne, coe_uIcc, Equiv.Perm.OnCycleFactors.centralizer_smul_def, Finpartition.mem_part, mem_finAntidiagonal, Polynomial.mem_nthRootsFinset, schnirelmannDensity_finset, coe_sigma, mem_Ico, isLeast_min', ClassGroup.exists_mem_finset_approx', fold_op_rel_iff_or, noncommProd_cons, mem_shatterer, isWF, ProbabilityTheory.Kernel.partialTraj_eq_prod, sum_dite, alternatingGroup.conj_smul_range_ofSubtype, mem_prod_list_ofFn, Set.biInter_finsetSigma_univ', piecewise_coe, not_disjoint_iff, left_mem_Ico, mem_uIcc, MeasureTheory.SimpleFunc.map_preimage_singleton, exists_mem_notMem_of_card_lt_card, inf'_le, image_mul_right, ProbabilityTheory.iIndepSets_singleton_iff, Ideal.Factors.piQuotientEquiv_map, ClassGroup.exists_mem_finsetApprox, Equiv.Perm.conj_smul_range_ofSubtype, Set.image_finset_prod_pi, Fin.attachFin_Ioc, notMem_compl, iSup_union, ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, ProbabilityTheory.iIndepFun.indepFun_finset, mulDissociated_iff_sum_eq_subsingleton, notMem_sigmaLift_of_ne_right, biSup_finsetSigma, continuous_restrict₂_apply, AddSemigroupIdeal.fg_iff, MvPolynomial.decomposition.decompose'_eq, Equiv.Perm.commute_ofSubtype_noncommPiCoprod, mem_of_subset, PairReduction.radius_logSizeBallSeq_zero, Set.coe_toFinset, coe_disjUnion, mem_insertNone, IsTopologicalBasis.iInf_induced, min_mem_insert_top_image_coe, zero_mem_smul_finset, insert_inj_on', LieAlgebra.IsKilling.instIsIrreducibleSubtypeWeightMemLieSubalgebraFinsetRootDualRootSystemOfIsSimple, RootPairing.Base.chainTopCoeff_eq_of_ne, mem_sum_list_ofFn, MeasureTheory.instIsZeroOrProbabilityMeasureForallValNatMemFinsetInducedFamilyOfForallIic, nsmul_right_strictMonoOn, AddMonoidAlgebra.mem_supported, alternatingGroup.ofSubtype_comp_subtype, CovBy.exists_finset_insert, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map, MonovaryOn.sum_comp_perm_mul_lt_sum_mul_iff, 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, ProbabilityTheory.Kernel.traj_eq_prod, Submodule.spanFinrank_eq_iInf, Holor.sum_unitVec_mul_slice, ssubset_iff_of_subset, IsApproximateAddSubgroup.of_small_tripling, List.cons_mem_fixedLengthDigits_succ, tsum_subtype', eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open, coe_subset, Finsupp.image_pow_eq_finsuppProd_image, PMF.toMeasure_apply_finset, interior_iInter, PartitionOfUnity.mem_finsupport, Finsupp.sym2_support_eq_preimage_support_mul, exists_subset_injOn_image_eq_of_surjOn, mem_upShadow_iterate_iff_exists_mem_card_add, insert_inter, mem_mul, mulIndicator_biUnion, HilbertBasis.finite_spans_dense, Polynomial.toSubring_one, ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul, SimpleGraph.Walk.exists_mem_support_forall_mem_support_imp_eq, Set.definable_iff_finitely_definable, List.mem_fixedLengthDigits_iff
partialOrder 📖	CompOp	473 math math: 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, disjUnion_singleton, 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, pairwiseDisjoint_disjUnion, disjoint_of_erase_right, tendsto_Ico_neg_atTop_atTop, add_sum_eq_sum_insertNone, pairwiseDisjoint_range_singleton, singleton_disjUnion, Icc_eq_image_powerset, grade_eq, isAtom_iff, cauchySeq_finset_iff_nat_tsum_vanishing, CategoryTheory.preservesFiniteColimits_liftToFinset, le_addRothNumber_product, disjoint_erase_insert, disjUnion_product, DFinsupp.disjoint_iff, disjoint_coe, pairwiseDisjoint_coe, SimpleGraph.isBipartiteWith_neighborFinset_disjoint, disjoint_union_right, Equiv.Perm.support_cycleOf_le, Turing.TM1.step_supports, 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, IsLowerSet.memberSubfamily, 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, SimpleGraph.interedges_disjoint_left, 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, SimpleGraph.CompleteEquipartiteSubgraph.disjoint, Equiv.Perm.support_pow_le, 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, disjiUnion_disjiUnion, erase_wcovBy, cauchySeq_finset_of_norm_bounded_eventually, Profinite.isIso_indexCone_lift, Ico_disjoint_Ico_consecutive, card_eraseNone_le, Rel.interedges_disjoint_left, 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, Turing.TM2.step_supports, 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, disjoint_preimage, 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, prod_anti_set_of_le_one', 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, disjoint_disjiUnion_right, covBy_cons, pairwiseDisjoint_iff, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset_obj_map, product_disjUnion, 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, IsLowerSet.nonMemberSubfamily, 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, pairwiseDisjoint_filter, card_Ico_finset, Equiv.Perm.support_mul_le, Monotone.tendsto_atTop_finset, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_map, not_addDissociated_iff_exists_disjoint, sum_anti_set_of_nonpos', 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, SimpleGraph.interedges_disjoint_right, disjoint_of_subset_left, sum_eraseNone, Filter.tendsto_finset_preimage_atTop_atTop, disjoint_of_erase_left, coe_eraseNone, le_mulRothNumber_product, nsmul_right_strictMono, Colex.toColex_mono, disjoint_disjiUnion_left, 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, Fintype.piFinset_disjoint_of_disjoint, 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, Rel.interedges_disjoint_right, 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, 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', Filter.tendsto_atTop_finset_of_monotone, 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, disjiUnion_map, 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, disjoint_filter_filter, Nat.disjoint_primeFactors, prod_insertNone, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app, shatterer_eq, instMulLeftMono, IsAddFreimanHom.addRothNumber_mono, pi_disjoint_of_disjoint, PreAbstractSimplicialComplex.isRelLowerSet_faces, 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, ArithmeticFunction.tendsTo_eulerProduct_of_tendsTo, 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, Disjoint.of_image_finset, Equiv.Perm.ofSubtype_support_disjoint, HasProdUniformlyOn.tendstoUniformlyOn, SummationFilter.LeAtTop.le_atTop, prod_mono_set_of_one_le, 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, disjoint_of_subset_right, 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, disjoint_disjUnion_left, 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, disjiUnion_cons, Icc_eq_filter_powerset, antitone_iff_forall_cons_le, cauchySeq_finset_of_geometric_bound, disjoint_disjUnion_right, 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, disjUnion_comm, 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, Equiv.Perm.disjoint_support_closure_of_disjoint_support, mulRothNumber_singleton, nsmul_right_strictMonoOn, prod_mono_set_of_one_le', val_covBy_val, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_map
toSet 📖	CompOp	—
val 📖	CompOp	128 math math: val_strictMono, range_val, insert_val, 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, AddMonoidAlgebra.supportedEquivFinsupp_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, Multiset.map_univ_coe, Multiset.map_univ_val_equiv, coe_toList, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, lcm_def, val_injective, 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, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, univ_val_map_subtype_restrict, Finpartition.ofSetoid_parts_val, inter_val_nd, Multiset.map_univ, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, 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, LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues, val_wcovBy_val, nodup_map_iff_injOn, pi_val, empty_val, Equiv.Perm.cycleType_def, erase_val, sup_def, card_def, Nat.val_divisorsAntidiagonal, 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, val_le_iff, noncommSum_lemma, mem_val, Polynomial.Chebyshev.roots_U_real, disjiUnion_val, mem_def, 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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_coeEmb 📖	mathematical	—	DFunLike.coe OrderEmbedding Finset Set Preorder.toLE PartialOrder.toPreorder partialOrder Set.instLE instFunLikeOrderEmbedding coeEmb SetLike.coe instSetLike	—	—
coe_inj 📖	mathematical	—	SetLike.coe Finset instSetLike	—	SetLike.coe_set_eq
coe_injective 📖	mathematical	—	Finset Set SetLike.coe instSetLike	—	—
coe_mem 📖	mathematical	—	Finset SetLike.instMembership instSetLike Set Set.instMembership SetLike.coe	—	—
coe_sort_coe 📖	mathematical	—	Set.Elem SetLike.coe Finset instSetLike SetLike.instMembership	—	—
coe_ssubset 📖	mathematical	—	Set Set.instHasSSubset SetLike.coe Finset instSetLike instHasSSubset	—	instIsConcreteLE
coe_subset 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Finset instSetLike instHasSubset	—	—
eq_of_veq 📖	—	val	—	—	—
exists_coe 📖	mathematical	—	Finset SetLike.instMembership instSetLike	—	—
exists_of_ssubset 📖	mathematical	Finset instHasSSubset	Finset SetLike.instMembership instSetLike	—	Set.exists_of_ssubset
ext 📖	—	Finset SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Finset SetLike.instMembership instSetLike	—	ext
forall_coe 📖	mathematical	—	Finset SetLike.instMembership instSetLike	—	—
forall_mem_not_eq 📖	mathematical	—	Finset SetLike.instMembership instSetLike	—	—
forall_mem_not_eq' 📖	mathematical	—	Finset SetLike.instMembership instSetLike	—	—
instAntisymmSubset 📖	mathematical	—	Finset instHasSubset	—	—
instAsymmSSubset 📖	mathematical	—	Finset instHasSSubset	—	—
instIrreflSSubset 📖	mathematical	—	Finset instHasSSubset	—	—
instIsNonstrictStrictOrderSubsetSSubset 📖	mathematical	—	IsNonstrictStrictOrder Finset instHasSubset instHasSSubset	—	—
instIsTransSSubset 📖	mathematical	—	IsTrans Finset instHasSSubset	—	—
instIsTransSubset 📖	mathematical	—	IsTrans Finset instHasSubset	—	—
instReflSubset 📖	mathematical	—	Finset instHasSubset	—	—
isWellFounded_ssubset 📖	mathematical	—	IsWellFounded Finset instHasSSubset	—	Subrelation.isWellFounded instIsWellFoundedInvImage Multiset.instWellFoundedLT val_lt_iff
le_eq_subset 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder partialOrder instHasSubset	—	—
le_iff_subset 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder partialOrder instHasSubset	—	—
lt_eq_subset 📖	mathematical	—	Finset Preorder.toLT PartialOrder.toPreorder partialOrder instHasSSubset	—	—
lt_iff_ssubset 📖	mathematical	—	Finset Preorder.toLT PartialOrder.toPreorder partialOrder instHasSSubset	—	—
mem_coe 📖	mathematical	—	Set Set.instMembership SetLike.coe Finset instSetLike SetLike.instMembership	—	—
mem_def 📖	mathematical	—	Finset SetLike.instMembership instSetLike Multiset Multiset.instMembership val	—	—
mem_mk 📖	mathematical	Multiset.Nodup	Finset SetLike.instMembership instSetLike Multiset Multiset.instMembership	—	—
mem_of_subset 📖	mathematical	Finset instHasSubset SetLike.instMembership instSetLike	Finset SetLike.instMembership instSetLike	—	Multiset.mem_of_subset
mem_val 📖	mathematical	—	Multiset Multiset.instMembership val Finset SetLike.instMembership instSetLike	—	—
mk_coe 📖	mathematical	Set Set.instMembership SetLike.coe Finset instSetLike	Set Set.instMembership SetLike.coe Finset instSetLike	—	Subtype.coe_eta
nodup 📖	mathematical	—	Multiset.Nodup val	—	—
notMem_mono 📖	mathematical	Finset instHasSubset SetLike.instMembership instSetLike	Finset SetLike.instMembership instSetLike	—	—
not_mem_subset 📖	mathematical	Finset instHasSubset SetLike.instMembership instSetLike	Finset SetLike.instMembership instSetLike	—	notMem_mono
not_subset 📖	mathematical	—	Finset instHasSubset SetLike.instMembership instSetLike	—	—
pairwise_subtype_iff_pairwise_finset 📖	mathematical	—	Pairwise Finset SetLike.instMembership instSetLike Function.onFun Set.Pairwise SetLike.coe	—	pairwise_subtype_iff_pairwise_finset'
pairwise_subtype_iff_pairwise_finset' 📖	mathematical	—	Pairwise Finset SetLike.instMembership instSetLike Function.onFun Set.Pairwise SetLike.coe	—	pairwise_subtype_iff_pairwise_set
setOf_mem 📖	mathematical	—	setOf Finset SetLike.instMembership instSetLike SetLike.coe	—	—
ssubset_def 📖	mathematical	—	Finset instHasSSubset instHasSubset	—	—
ssubset_iff_of_subset 📖	mathematical	Finset instHasSubset	Finset instHasSSubset SetLike.instMembership instSetLike	—	Set.ssubset_iff_of_subset
ssubset_iff_subset_ne 📖	mathematical	—	Finset instHasSSubset instHasSubset	—	lt_iff_le_and_ne
ssubset_of_ssubset_of_subset 📖	mathematical	Finset instHasSSubset instHasSubset	Finset instHasSSubset	—	Set.ssubset_of_ssubset_of_subset
ssubset_of_subset_of_ssubset 📖	mathematical	Finset instHasSubset instHasSSubset	Finset instHasSSubset	—	Set.ssubset_of_subset_of_ssubset
subset_def 📖	mathematical	—	Finset instHasSubset Multiset Multiset.instHasSubset val	—	—
subset_iff 📖	mathematical	—	Finset instHasSubset SetLike.instMembership instSetLike	—	—
subset_iff_notMem 📖	mathematical	—	Finset instHasSubset SetLike.instMembership instSetLike	—	—
subset_of_eq 📖	mathematical	—	Finset instHasSubset	—	Subset.refl
subset_of_le 📖	mathematical	Finset Preorder.toLE PartialOrder.toPreorder partialOrder	Finset instHasSubset	—	—
val_inj 📖	mathematical	—	val	—	val_injective
val_injective 📖	mathematical	—	Finset Multiset val	—	eq_of_veq
val_le_iff 📖	mathematical	—	Multiset Preorder.toLE PartialOrder.toPreorder Multiset.instPartialOrder val Finset instHasSubset	—	Multiset.le_iff_subset nodup
val_lt_iff 📖	mathematical	—	Multiset Preorder.toLT PartialOrder.toPreorder Multiset.instPartialOrder val Finset instHasSSubset	—	val_le_iff
val_strictMono 📖	mathematical	—	StrictMono Finset Multiset PartialOrder.toPreorder partialOrder Multiset.instPartialOrder val	—	val_lt_iff
wellFoundedLT 📖	mathematical	—	WellFoundedLT Finset Preorder.toLT PartialOrder.toPreorder partialOrder	—	isWellFounded_ssubset

Finset.FinsetCoe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift Finset SetLike.instMembership Finset.instSetLike	—	—

Finset.PiFinsetCoe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift Finset SetLike.instMembership Finset.instSetLike	—	PiSubtype.canLift
canLift' 📖	mathematical	—	CanLift Finset SetLike.instMembership Finset.instSetLike	—	canLift

Finset.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antisymm 📖	—	Finset Finset.instHasSubset	—	—	Finset.ext
antisymm_iff 📖	mathematical	—	Finset Finset.instHasSubset	—	le_antisymm_iff
refl 📖	mathematical	—	Finset Finset.instHasSubset	—	Multiset.Subset.refl
rfl 📖	mathematical	—	Finset Finset.instHasSubset	—	refl
trans 📖	mathematical	Finset Finset.instHasSubset	Finset Finset.instHasSubset	—	Multiset.Subset.trans

Finset.Superset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trans 📖	mathematical	Finset Finset.instHasSubset	Finset Finset.instHasSubset	—	Finset.Subset.trans

List

Definitions

Name	Category	Theorems
instDecidableMapsToCoeFinsetOfDecidablePredMemSet 📖	CompOp	—
instDecidableSurjOnCoeFinsetOfDecidableEq 📖	CompOp	—

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLiftFinset 📖	mathematical	—	CanLift Multiset Finset Finset.val Nodup	—	—

---

← Back to Index