| Name | Category | Theorems |
|---|
filterMap 📖 | CompOp | 7 mathmath: filterMap_mono, filterMap_val, List.toFinset_filterMap, mem_filterMap, coe_filterMap, filterMap_empty, filterMap_some
|
image 📖 | CompOp | 507 mathmath: Fin.finsetImage_castLE_Iio, image_image₂, set_biInter_finset_image, image_subset_infs_left, Fin.finsetImage_natAdd_Ioc, pimage_eq_image_filter, Nat.smoothNumbersUpTo_subset_image, Nat.antidiagonal_eq_image', mem_zpowers_iff_mem_range_orderOf, Fintype.coe_image_univ, Fintype.piFinset_image, MvPolynomial.support_finSuccEquiv, IsCyclic.image_range_orderOf, biUnion_image_sdiff_left, Fin.finsetImage_castLE_Ioo, image₂_curry, image_subset_diffs_right, singleton_sub, image_vadd_comm, image_op_inv, mem_range_iff_mem_finset_range_of_mod_eq, Fin.finsetImage_addNat_Ioi, image_neg, product_image_fst, biUnion_image_sdiff_right, subset_product_image_snd, image_orderEmbOfFin_univ, Fin.finsetImage_castAdd_uIcc, mem_image_const, image_uncurry_product, Fin.finsetImage_addNat_Ici, sigma_image_fst_preimage_mk, biUnion_image_left, finrank_vectorSpan_image_finset_le, image_injective, Fin.finsetImage_castSucc_Ioo, image_empty, Nat.image_Ico_mod, Icc_eq_image_powerset, exists_of_one_lt_card_pi, Fin.finsetImage_castSucc_uIcc, image_image₂_antidistrib_right, Fin.finsetImage_natAdd_Icc, Fin.image_succ_univ, image_smul_product, Fin.finsetImage_val_Ioi, image_inter_of_injOn, Fin.univ_image_getElem', Nat.image_sub_const_Ico, IsAddCyclic.image_range_addOrderOf, biUnion_image, image_smul_distrib, Fin.finsetImage_val_Ioo, Set.toFinset_range, map_ofDual_max, image_univ_equiv, image_congr, image_const, memberSubfamily_image_erase, powerset_insert, Nat.antidiagonal_eq_image, Nat.Ico_image_const_sub_eq_Ico, univ_filter_exists, image_diag, set_biUnion_finset_image, Sym2.filter_image_mk_isDiag, image_range_addOrderOf, mem_image_univ_iff_mem_range, Finsupp.mapDomain_support_of_injective, image₂_subset_iff_right, Finsupp.mapDomain_support_of_injOn, Fin.finsetImage_castAdd_Iio, mem_image, Fin.finsetImage_castSucc_Ioc, image_inj, Nonempty.image, disjoint_image, image_mul_left', image_div_product, IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf, dens_eq_sum_dens_image, UniqueMul.mulHom_image_iff, Finsupp.mapDomain_support, image_swap_product, sum_image_of_pairwise_eq_zero, image_add_left_Ioo, fold_image_idem, product_image_snd, sum_image_le_of_nonneg, toLeft_image_swap, Fin.finsetImage_castAdd_Iic, Fin.finsetImage_succ_Iio, image_subset_image_iff, image_toFinset, expect_image, image_surjOn_powerset, piAntidiag_insert, attach_insert, image_vadd_distrib, List.fixedLengthDigits_one, Fin.finsetImage_castLE_Ico, toDual_min', image_nonempty, Fin.finsetImage_succ_Ico, seq_def, map_comp_coe_apply, image_add_right, image_eq_empty, image₂_insert_left, Module.Basis.reindexFinsetRange_apply, smul_singleton, Colex.toColex_image_lt_toColex_image, AddMonoid.exponent_eq_max'_addOrderOf, SimpleGraph.edgeFinset_replaceVertex_of_adj, image_op_one, BoxIntegral.Prepartition.sum_fiberwise, image_pow_of_ne_zero, MvPolynomial.support_rename_of_injective, Fin.finsetImage_castAdd_Ico, image_subset_sups_left, product_eq_biUnion, sups_singleton, Fin.finsetImage_cast_Ioi, AddMonoidAlgebra.support_mul_single_subset, image_nsmul_of_ne_zero, support_of_fiberwise_sum_subset_image, image_inter, singleton_diffs, gcd_image, image_univ_of_surjective, prod_image_of_pairwise_eq_one, IsOfFinOrder.mem_powers_iff_mem_range_orderOf, MvPolynomial.support_expand_subset, Fin.finsetImage_cast_Iio, Fin.finsetImage_val_Iio, image₂_image_left, Sym2.card_image_diag, AddMonoidAlgebra.support_single_mul_subset, nonMemberSubfamily_image_insert, FiniteField.card_image_polynomial_eval, Polynomial.roots_expand_image_frobenius, Fin.finsetImage_cast_Icc, image_comm, image_image₂_distrib_right, fiber_nonempty_iff_mem_image, image_zero, inf_image, SimpleGraph.edgeFinset_replaceVertex_of_not_adj, map_toDual_max, Fin.finsetImage_castAdd_Ici, Fin.finsetImage_cast_Ici, image_pow, div_def, image_id, singleton_infs, MonoidAlgebra.support_mul_single_eq_image, Function.Commute.finset_image, max_mem_image_coe, image_mul, coe_image_subset_range, SkewMonoidAlgebra.support_mul_single_eq_image, Nonempty.ciSup_mem_image, image_union, IsAddCyclic.image_range_card, coe_image, vectorSpan_eq_span_vsub_finset_right_ne, IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf, prod_partition, Fin.finsetImage_castSucc_Ico, image_subset_sups_right, Fin.finsetImage_addNat_Ioc, vadd_finset_def, SkewMonoidAlgebra.support_single_mul_eq_image, image_subset_diffs_left, image_add_right', sum_comp, prod_comp, SSet.stdSimplex.face_obj, max_mem_insert_bot_image_coe, image_some_eraseNone, Fin.finsetImage_succ_uIcc, Fin.finsetImage_rev_Iic, image_singleton, Fin.finsetImage_val_Ioc, partialSups_eq_sUnion_image, Int.image_Ico_emod, Monotone.map_finset_min', Nat.image_div_divisors_eq_divisors, image_sub_product, mem_powers_iff_mem_range_orderOf, Ico_eq_image_ssubsets, univ_filter_mem_range, Fin.finsetImage_castLE_uIcc, Fin.finsetImage_rev_Ioc, powerset_image, image_smul_comm, map_toDual_min, Polynomial.roots_expand_image_frobenius_subset, mem_image_const_self, card_nsmul_quotient_add_nsmul_inter_addSubgroup_le, Function.Injective.mem_finset_image, Fin.finsetImage_rev_Ioi, memberSubfamily_image_insert, AffineIndependent.finrank_vectorSpan_image_finset, Fin.finsetImage_succ_Iic, Polynomial.reflect_support, min_mem_image_coe, memberSubfamily_union_nonMemberSubfamily, Fin.finsetImage_rev_uIcc, Fin.univ_image_get', card_image_of_injective, Nat.image_snd_divisorsAntidiagonal, finsum_mem_finset_product', Set.toFinset_image, MonoidAlgebra.support_mul_single_subset, Fin.finsetImage_castAdd_Ioi, SupIndep.image, Fin.finsetImage_natAdd_Ico, prod_image_le_of_one_le, toRight_image_swap, card_eq_sum_card_image, Fin.finsetImage_val_Ico, image_sdiff_product, image_op_zero, image_subset_iff_subset_preimage, ciInf_mem_image, mem_range_iff_mem_finset_range_of_mod_eq', SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image, range_image_pred_top_sub, product_eq_biUnion_right, sub_singleton, AddMonoidAlgebra.support_mul_single_eq_image, canLift, iInf_finset_image, image_subset_Iic_sup, Fin.finsetImage_cast_Ioo, sum_image_of_disjoint, Module.Basis.reindexFinsetRange_repr_self, card_le_mul_card_image, Fin.finsetImage_val_Ici, Nat.image_piFinTwoEquiv_finMulAntidiag, image_inv_eq_inv, Fin.univ_image_get, subset_product_image_fst, toDual_max', finprod_mem_finset_product', UniqueAdd.addHom_image_iff, image_vadd, Set.Finite.toFinset_range, image_add_product, SimpleGraph.dart_fst_fiber, Fin.finsetImage_addNat_Ico, image_op_mul, neg_def, mul_card_image_le_card, image_injOn_powerset_of_injOn, BoxIntegral.integralSum_fiberwise, card_image_le, Set.PairwiseDisjoint.image_finset_of_le, erase_image_subset_image_erase, inf'_comp_eq_image, DomMulAct.stabilizer_card', Submodule.span_range_natDegree_eq_adjoin, prod_image', lcm_eq_lcm_image, image_subset_iff, Set.Finite.toFinset_image, image_smul, prodMap_image_product, image_nsmul, image_preimage, IsCyclic.image_range_card, image_subset_image₂_left, Fintype.eval_image_piFinset_subset, Fin.image_castSucc, subset_set_image_iff, SkewMonoidAlgebra.support_mul_single_subset, IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf, image_inter_subset, image_infs, dens_image, Fin.finsetImage_succ_Ioo, Nat.image_fst_divisorsAntidiagonal, Fin.univ_image_def, image₂_image_left_anticomm, Fin.finsetImage_castSucc_Ioi, MvPolynomial.image_support_finSuccEquiv, MvPolynomial.support_expand, Fin.finsetImage_natAdd_Ioi, image_subset_image, sup_singleton_apply, fold_image, image_image₂_antidistrib, sub_def, imageAddHom_apply, Matrix.BlockTriangular.det, Fin.finsetImage_val_Icc, biUnion_image_sup_right, image_subset_infs_right, le_card_quotient_mul_sq_inter_subgroup, MonoidAlgebra.support_single_mul_eq_image, le_card_quotient_add_sq_inter_addSubgroup, image_id', image₂_singleton_left, image_sup_product, Monoid.exponent_eq_max'_orderOf, image_val_attachFin, map_eq_image, image_sdiff_of_injOn, smul_finset_def, subset_univ_image_iff, MvPolynomial.support_optionEquivLeft, image_diag_union_image_offDiag, smul_def, sup_image, ofDual_min', infs_singleton, mem_zmultiples_iff_mem_range_addOrderOf, pimage_some, lcm_image, biUnion_image_inf_right, imageMulHom_apply, image_add_right_Ico, image_biUnion, Sym2.filter_image_mk_not_isDiag, Fin.finsetImage_castSucc_Iic, biUnion_image_sup_left, Fin.finsetImage_castSucc_Icc, singleton_vsub, exists_mem_image, MvPolynomial.weightedDecomposition.decompose'_eq, biUnion_image_right, image₂_subset_iff_left, Fin.finsetImage_succ_Icc, Fin.finsetImage_rev_Iio, IsOfFinAddOrder.multiples_eq_image_range_addOrderOf, image_add_right_Icc, Function.Semiconj.finset_image, image₂_image_left_comm, sym2_insert, eraseNone_image_some, OrthonormalBasis.span_apply, image_preimage_of_bij, div_singleton, card_image_iff, Fin.finsetImage_addNat_Icc, Polynomial.Chebyshev.roots_T_real, image_range_orderOf, image_mul_product, MvPolynomial.coeffs_map, diffs_singleton, Fin.finsetImage_rev_Icc, image_insert_memberSubfamily, image_val_of_injOn, Sym2.card_image_offDiag, restrict_preimage, card_pow_quotient_mul_pow_inter_subgroup_le, image_add_left', image_neg_eq_neg, Colex.toColex_image_ofColex_strictMono, image₂_singleton_left', range_sdiff_zero, attach_affineCombination_of_injective, SkewMonoidAlgebra.support_single_mul_subset, image₂_singleton_right, image_inv, Polynomial.degreeLT_eq_span_X_pow, iSup_finset_image, AddMonoidAlgebra.support_single_mul_eq_image, card_image_of_injOn, image_subset_image₂_right, MvPolynomial.vars_rename, Finsupp.image_fst_graph, gcd_eq_gcd_image, Polynomial.roots_expand_image_iterateFrobenius, Colex.toColex_image_le_toColex_image, sup'_comp_eq_image, sum_image, image_add_right_Ioc, Fin.finsetImage_val_Iic, Fin.finsetImage_succ_Ici, SimpleGraph.disjoint_sdiff_neighborFinset_image, Fin.finsetImage_castLE_Iic, shatters_iff, image_op_add, Monotone.map_finset_max', imageOneHom_apply, UV.compress_disjoint, Polynomial.roots_expand_pow_image_iterateFrobenius_subset, IsOfFinOrder.powers_eq_image_range_orderOf, Fin.finsetImage_natAdd_uIcc, subset_image_iff, Fin.finsetImage_val_uIcc, image_add_right_Ioo, image_biUnion_filter_eq, Fin.finsetImage_addNat_Ioo, singleton_sups, filter_image, Fintype.eval_image_piFinset_const, biUnion_singleton, Fin.finsetImage_castSucc_Ici, Fin.finsetImage_rev_Ico, image_add_left_Icc, image_add, image_op_pow, mem_multiples_iff_mem_range_addOrderOf, Fin.finsetImage_castSucc_Iio, Multiset.toFinset_map, Nat.image_apply_finMulAntidiag, image₂_insert_right, MeasureTheory.lmarginal_image, Behrend.threeAPFree_image_sphere, Fin.finsetImage_cast_Iic, image_sups, Fin.finsetImage_castAdd_Icc, image_mono, mulSupport_of_fiberwise_prod_subset_image, Fin.finsetImage_castLE_Ioc, Sym2.two_mul_card_image_offDiag, map_ofDual_min, subset_product, mul_def, sym_succ, Fin.finsetImage_natAdd_Ioo, mem_image_of_mem, image_erase, fiber_card_ne_zero_iff_mem_image, SimpleGraph.copyCount_eq_card_image_copyToSubgraph, range_pow_padicValNat_subset_divisors', image_val, Fin.finsetImage_cast_Ioc, image_subtype_ne_univ_eq_image_erase, sum_partition, image_one, vadd_singleton, image_image, image_image₂_right_comm, image_add_left_Ico, Fin.finsetImage_cast_Ico, add_def, Polynomial.degreeLE_eq_span_X_pow, Fin.image_succAbove_univ, Fin.finsetImage_castAdd_Ioo, inv_def, MonoidAlgebra.support_single_mul_subset, Fin.finsetImage_natAdd_Ici, Fin.finsetImage_rev_Ioo, Fin.finsetImage_cast_uIcc, Multiset.image_toEnumFinset_fst, Fin.finsetImage_succ_Ioc, biUnion_image_inf_left, image_div, HahnSeries.SummableFamily.support_powerSeriesFamily_subset, sum_image', sym2_image, MvPolynomial.support_esymm, Fin.finsetImage_castAdd_Ioc, image_mul_right', fmap_def, image_op_nsmul, powersetCard_succ_insert, image_add_left, vadd_def, MeasureTheory.SimpleFunc.range_map, Fintype.eval_image_piFinset, ofDual_max', ciSup_mem_image, image_compl, Finsupp.support_curry, image_add_left_Ioc, Filter.tendsto_finset_image_atTop_atTop, image_image₂_right_anticomm, image_image₂_distrib_left, Fin.finsetImage_addNat_uIcc, image_vadd_product, range_pow_padicValNat_subset_divisors, Fin.finsetImage_rev_Ici, pi_insert, vsub_singleton, Matrix.BlockTriangular.charpoly, image_ssubset_image, attach_image_val, Polynomial.Chebyshev.roots_U_real, image_insert, Fin.finsetImage_succ_Ioi, Subgroup.closure_mul_image_eq_top', sym2_eq_image, image_image₂_antidistrib_left, image_mul_left, image_symmDiff, prod_image_of_disjoint, image_op_neg, image_image₂_distrib, Finpartition.parts_inf, image_mul_right, singleton_div, prod_image, image₂_image_right, MvPolynomial.decomposition.decompose'_eq, imageZeroHom_apply, min_mem_insert_top_image_coe, image_inf_product, Fin.finsetImage_castLE_Icc, Finpartition.ofSetSetoid_parts, exists_subset_injOn_image_eq_of_surjOn, HilbertBasis.finite_spans_dense, image_sdiff
|
map 📖 | CompOp | 470 mathmath: map_nsmul_piAntidiag_univ, AffineIndependent.indicator_extend_eq_of_affineCombination_comp_embedding_eq, weightedVSubOfPoint_map, SkewMonoidAlgebra.domCongr_support, Fin.univ_map_def, Fin.map_succEmb_Iio, map_op_one, sum_map', toLeft_map_sumComm, disjoint_map, Fin.Ioi_succ, prod_map', map_filter', Sigma.Ici_mk, subtype_map_of_mem, PNat.map_subtype_embedding_Ico, map_zero, attach_cons, Sum.Lex.Icc_inr_inr, WithTop.Ico_coe_coe, toLeft_eq_univ, Fin.map_castLEEmb_Ioc, product_self_eq_disjiUnion_perm_aux, Ioo_map_sectR, Set.powersetCard.val_ofFinEmb, Fin.map_revPerm_Ioc, Fin.map_castAddEmb_Ico, Nat.Ioc_filter_modEq_cast, uIcc_toDual, Icc_map_sectL, SkewMonoidAlgebra.support_single_mul, dens_map_le, uIcc_map_sectR, map_filter, Rel.interedges_eq_biUnion, Nat.divisors_prime_pow, Ioi_toDual, WithTop.Ioc_coe_coe, Fin.map_castLEEmb_Iic, WithTop.Ico_coe_top, Sum.Lex.Ico_inl_inl, product_singleton, Sum.Lex.Ico_inr_inr, Fin.map_addNatEmb_Ici, Nat.antidiagonal_succ_succ', UniqueAdd.iff_addOpposite, Sum.Lex.Ioo_inl_inr, Function.Embedding.exists_of_card_eq_finset, SimpleGraph.map_edgeFinset_induce_of_support_subset, map_truncatedInf, SkewMonoidAlgebra.support_mul_single, Sum.Ico_inl_inl, range_add_one', Multiset.Icc_eq, map_op_inv, dens_map_equiv, Fin.map_natAddEmb_Ici, disjSum_empty, map_consEquiv_filter_piFinset, Affine.Simplex.excenterWeightsUnnorm_reindex, inf_map, Sum.Lex.Iic_inr, WithTop.Ioo_coe_top, Fin.map_castLEEmb_uIcc, Nat.map_swap_divisorsAntidiagonal, weightedVSub_map, map_snocEquiv_filter_piFinset, Finpartition.parts_bot, SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map, Nat.map_div_left_divisors, mulRothNumber_map_mul_left, Sum.Iio_inr, Fin.map_valEmbedding_uIcc, map_nsmul_piAntidiag, Nat.antidiagonal_eq_map, Nat.antidiagonal_succ, Ioc_ofDual, Affine.Simplex.excenterExists_reindex, Fin.map_succEmb_uIcc, Sum.Lex.Ioo_inr_inr, map_symm_subset, Fin.map_addNatEmb_Ioi, subset_map_inl, Function.Semiconj.finset_map, Fin.map_castAddEmb_Ici, Fin.map_finCongr_Ioo, Finpartition.parts_map, subtype_map, range_add, map_sym_eq_piAntidiag, Function.Commute.finset_map, Sigma.Iic_mk, hasSum_support, Ioo_orderDual_def, map_nontrivial, WithBot.Ioc_bot_coe, centroid_map, Nonempty.map, SimpleGraph.edgeFinset_map, WithTop.Icc_coe_coe, SimpleGraph.cliqueSet_map_of_equiv, card_map, Sum.Ici_inr, SimpleGraph.isClique_map_finset_iff, sum_map, Fin.map_natAddEmb_uIcc, toRight_map_sumComm, Fin.univ_succAbove, Int.map_prodComm_divisorsAntidiag, WithTop.Ioo_coe_coe, Fin.map_finCongr_Iic, ContextFreeGrammar.reverse_rules, Finsupp.antidiagonal_single, FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_snd_coe, Fin.map_revPerm_Ico, Nat.antidiagonalTuple_two, Sum.Lex.Icc_inl_inl, Ioo_ofDual, map_op_nsmul, Sum.Icc_inr_inr, Affine.Simplex.excenterWeights_reindex, Fin.map_castLEEmb_Ico, SimpleGraph.IsNClique.of_induce, Sigma.Ico_mk_mk, map_subtype_subset, Sum.Ioc_inr_inr, map_one, Sum.Lex.Ioi_inr, Sum.Ioi_inr, Iio_orderDual_def, Int.divisorsAntidiag_natCast, Int.Ioo_eq_finset_map, SimpleGraph.IsNClique.map, sumLexLift_inl_inl, map_univ_equiv, UniqueMul.iff_mulOpposite, Fin.map_revPerm_Ici, Sum.Iio_inl, gc_map_inr_toRight, Fin.map_castLEEmb_Ioo, Sum.Lex.Ici_inl, Affine.Simplex.exsphere_reindex, univ_map_equiv_to_embedding, Sigma.Icc_mk_mk, Sum.Lex.Ioc_inl_inl, univ_perm_option, mapRange_finsuppAntidiag_eq, map_insert, Fin.map_revPerm_Icc, filter_piFinset_eq_map_consEquiv, SimpleGraph.cliqueFinset_map_of_equiv, map_sdiff, map_inl_disjUnion_map_inr, Nat.properDivisors_prime_pow, PNat.map_subtype_embedding_Icc, map_add_left_Ico, SimpleGraph.cliqueSet_map, sym2_map, Fin.map_finCongr_uIcc, powersetCard_map, map_op_add, SimpleGraph.isClique_map_finset_iff_of_nontrivial, map_ssubset_map, Sum.Lex.Ioc_inl_inr, Sum.Lex.Iio_inl, Fin.map_revPerm_Ioi, Fin.Iio_last_eq_map, Fin.map_addNatEmb_Ico, Ioc_map_sectL, Fin.map_castLEEmb_Icc, Fin.map_valEmbedding_Ici, Affine.Simplex.exradius_reindex, map_subtype_embedding_Ioi, Ioi_orderDual_def, eraseNone_map_some, Fin.map_succEmb_Ioi, SimpleGraph.map_neighborFinset_induce_of_neighborSet_subset, Equiv.Perm.support_ofSubtype, Fin.map_finCongr_Ici, affineCombination_map, Sum.Ioo_inr_inr, Icc_orderDual_def, sup'_comp_eq_map, Ioo_toDual, filter_piFinset_eq_map_insertNthEquiv, Multiset.uIcc_eq, Affine.Simplex.touchpointWeights_reindex, map_toFinset, toLeft_eq_empty, SimpleGraph.IsClique.finsetMap, map_comm, map_op_zero, Set.Intersecting.disjoint_map_compl, map_op_neg, disjoint_map_inl_map_inr, Equiv.Perm.support_extend_domain, Multiset.map_univ_coeEmbedding, Sum.Lex.Ioc_inr_inr, Int.Icc_eq_finset_map, map_nonempty, SimpleGraph.cliqueFinset_map, Finsupp.support_embSigma, map_injective, Iic_orderDual_def, uIcc_map_sectL, PNat.map_subtype_embedding_Ioo, MvPolynomial.support_mul_X, Fin.map_succEmb_Ici, Sigma.Iio_mk, pairwiseDisjoint_map_sigmaMk, Fin.map_natAddEmb_Icc, Sum.Lex.Ioi_inl, mapRange_finsuppAntidiag_subset, Int.Ioc_eq_finset_map, toRight_eq_univ, Nat.map_div_right_divisors, disjiUnion_singleton, Sum.Lex.Ioo_inl_inl, Ico_ofDual, mem_map_mk, Ioc_orderDual_def, Nat.Ico_filter_modEq_cast, map_subtype_embedding_Ioc, Fin.map_valEmbedding_Icc, Fin.map_castSuccEmb_Ici, Equiv.finsetCongr_apply, Ioc_toDual, Sum.Lex.Iic_inl, Fin.map_natAddEmb_Ico, mem_map_equiv, map_add_left_Ioo, disjoint_range_addLeftEmbedding, Fin.univ_succ, Icc_toDual, sym2_cons, hasProd_support, Sigma.Ioc_mk_mk, Sum.Ioo_inl_inl, UniqueAdd.addHom_map_iff, Sum.Lex.Ici_inr, Ioo_map_sectL, prodMap_map_product, Int.uIcc_eq_finset_map, sup_map, Sigma.Ioi_mk, Sum.Ici_inl, PNat.map_subtype_embedding_uIcc, SimpleGraph.map_neighborFinset_induce, map_univ_of_surjective, piAntidiag_cons, Ioi_ofDual, Fin.map_castAddEmb_Ioc, MonoidAlgebra.support_mul_single, map_truncatedSup, Fin.map_revPerm_Ioo, Fin.map_revPerm_uIcc, map_add_right_Ico, Set.powersetCard.coe_addActionHom_of_embedding, Equiv.finsetSubtypeComm_symm_apply, univ_perm_fin_succ, fold_map, map_inl_subset_iff_subset_toLeft, Ici_toDual, Fin.map_valEmbedding_Ioi, map_op_mul, Sum.Lex.Ico_inl_inr, supIndep_map, map_cons, Fin.map_castLEEmb_Iio, Fin.map_addNatEmb_uIcc, Sum.Lex.Iio_inr, Sum.Iic_inl, LaurentPolynomial.toLaurent_support, sum_subtype_map_embedding, addRothNumber_map_add_left, Ioc_map_sectR, Fin.map_succEmb_Ioo, Affine.Simplex.touchpoint_reindex, pairwiseDisjoint_piAntidiag_map_addRightEmbedding, map_insertNthEquiv_filter_piFinset, Fin.map_valEmbedding_Ioo, subset_map_iff, map_subtype_embedding_Iio, map_eq_image, Icc_ofDual, SimpleGraph.isNClique_map_copy_top, Fin.map_castSuccEmb_Icc, Iio_toDual, Fin.Iio_castSucc, Fin.map_castAddEmb_Iio, Affine.Simplex.range_face_reindex, map_add_left_Ioc, map_refl, AddMonoidAlgebra.domCongr_support, Equiv.Perm.support_conj, Iic_ofDual, Fin.map_castAddEmb_uIcc, map_inr_subset_iff_subset_toRight, map_add_right_Ioo, toRight_eq_empty, map_add_right_Ioc, Sum.Ico_inr_inr, map_swap_antidiagonal, FirstOrder.Language.distinctConstantsTheory_eq_iUnion, Fin.map_natAddEmb_Ioi, Fin.map_valEmbedding_Ico, map_subtype_embedding_Ici, Fin.map_castSuccEmb_Iio, map_inj, MonoidAlgebra.support_single_mul, Sum.Iic_inr, Fin.map_revPerm_Iio, Fin.map_castSuccEmb_uIcc, Fin.map_succEmb_Ico, map_sups, sum_map_equiv, filter_piFinset_eq_map_snocEquiv, SimpleGraph.isNClique_map_iff, map_val, disjiUnion_map, map_singleton, map_valEmbedding_attachFin, Fin.map_castSuccEmb_Iic, Fin.map_finCongr_Ioi, Int.Ioc_filter_dvd_eq, Fin.map_addNatEmb_Ioc, Equiv.finsetSubtypeComm_apply_coe, Fin.map_succEmb_Ioc, UniqueMul.to_mulOpposite, map_add_left_Icc, map_disjSum, map_orderEmbOfFin_univ, prod_subtype_map_embedding, range_add_eq_union, Ico_orderDual_def, map_swap_product, Nat.antidiagonal_filter_le_fst_of_le, Finsupp.cons_support, Int.Ico_eq_finset_map, AddMonoidAlgebra.support_single_mul, inf'_comp_eq_map, Fin.map_valEmbedding_univ, Finsupp.extendDomain_support, Nat.antidiagonal_filter_snd_le_of_le, Int.divisorsAntidiag_neg, WithBot.Ico_coe_coe, Equiv.Perm.cycleFactorsFinset_conj, mem_map', mapEmbedding_apply, Int.divisorsAntidiag_ofNat, map_infs, Ico_map_sectR, Finsupp.piecewise_support, subset_map_symm, subset_map_inr, map_subset_iff_subset_preimage, SimpleGraph.isNIndepSet_induce, map_erase, WithBot.Ioo_coe_coe, sigma_eq_biUnion, map_add_right_Icc, Fin.univ_castSuccEmb, finsuppAntidiag_insert, SummationFilter.map_filter, Iic_toDual, MonoidAlgebra.domCongr_support, map_empty, singleton_product, coe_map, map_subtype_embedding_Ico, Ici_orderDual_def, Fin.map_castSuccEmb_Ioi, WithBot.Ioo_bot_coe, Fin.map_succEmb_Icc, algebraicIndependent_finset_map_embedding_subtype, prod_map, Fin.map_finCongr_Iio, linearIndependent_finset_map_embedding_subtype, preimage_map, UniqueMul.mulHom_map_iff, Fin.map_castSuccEmb_Ico, mem_map, Fin.map_addNatEmb_Icc, Fin.map_castSuccEmb_Ioo, map_cast_heq, Finsupp.support_embDomain, Ico_map_sectL, Nat.antidiagonal_eq_map', Int.Ico_filter_modEq_eq, Int.Ioc_filter_modEq_eq, StrictMonoOn.map_finsetSort, filter_attach, map_eq_empty, univ_map_embedding, Sum.Ioi_inl, Nat.antidiagonal_filter_fst_le_of_le, attach_map_val, map_sort, addRothNumber_map_add_right, WithBot.Ioc_coe_coe, Fin.map_castAddEmb_Iic, filter_attach', map_subset_map, empty_disjSum, Fin.map_valEmbedding_Iio, sumLexLift_inr_inr, Fin.Ioi_zero_eq_map, Fin.map_finCongr_Ioc, mem_map_of_mem, Fin.map_natAddEmb_Ioo, UniqueAdd.to_addOpposite, map_subtype_embedding_Ioo, Set.powersetCard.val_map, Nat.antidiagonal_filter_le_snd_of_le, Fin.map_addNatEmb_Ioo, map_union, AlternatingGroup.map_subtype_of_cycleType, PNat.map_subtype_embedding_Ioc, map_map, mulRothNumber_map_mul_right, disjoint_range_addRightEmbedding, Sum.Ioc_inl_inl, Fin.map_castAddEmb_Icc, Fin.map_castAddEmb_Ioo, map_inter, prod_map_equiv, product_self_eq_disjiUnion_perm, Sigma.Ioo_mk_mk, Fin.map_natAddEmb_Ioc, SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint, Sum.Lex.Icc_inl_inr, powersetCard_one, Fin.map_castSuccEmb_Ioc, Affine.Simplex.excenter_reindex, prod_comp_equiv, apply_coe_mem_map, map_op_pow, gc_map_inl_toLeft, Fin.map_revPerm_Iic, Int.Ico_filter_dvd_eq, Set.powersetCard.coe_mulActionHom_of_embedding, filter_map, MvPolynomial.support_X_mul, WithBot.Icc_coe_coe, SimpleGraph.map_edgeFinset_induce, Fin.map_finCongr_Icc, Fin.map_succEmb_Iic, sum_comp_equiv, notMem_map_subtype_of_not_property, map_subtype_embedding_Iic, AddMonoidAlgebra.support_mul_single, Ico_toDual, Int.divisorsAntidiag_neg_natCast, Fin.map_finCongr_Ico, map_some_eraseNone, map_subtype_embedding_Icc, Fin.map_valEmbedding_Iic, Icc_map_sectR, univ_map_subtype, Nat.antidiagonal_succ', Iio_ofDual, Fin.map_valEmbedding_Ioc, Ici_ofDual, Int.map_neg_divisorsAntidiag, map_perm, Sum.Icc_inl_inl, map_prodComm_antidiagonal, disjiUnion_map_sigma_mk, Fin.map_castAddEmb_Ioi, coe_map_subset_range
|
mapEmbedding 📖 | CompOp | 3 mathmath: Equiv.finsetCongr_toEmbedding, powersetCard_map, mapEmbedding_apply
|
subtype 📖 | CompOp | 31 mathmath: subtype_map_of_mem, PNat.Icc_eq_finset_subtype, PNat.Ioo_eq_finset_subtype, subtype_Ioc_eq, DFinsupp.support_subtypeDomain, subtype_mono, sum_subtype_of_mem, subtype_Ico_eq, prod_subtype_of_mem, DFinsupp.subtypeDomain_def, subtype_map, subtype_eq_univ, PNat.Ico_eq_finset_subtype, subtype_Iio_eq, PNat.uIcc_eq_finset_subtype, PNat.Ioc_eq_finset_subtype, Finsupp.support_subtypeDomain, mem_subtype, subtype_eq_empty, sum_subtype_eq_sum_filter, card_subtype, subtype_Iic_eq, subtype_Ici_eq, weightedVSub_subtype_eq_filter, prod_subtype_eq_prod_filter, weightedVSubOfPoint_subtype_eq_filter, subtype_univ, subtype_Ioo_eq, subtype_Icc_eq, affineCombination_subtype_eq_filter, subtype_Ioi_eq
|