| Name | Category | Theorems |
|---|
cons π | CompOp | 79 mathmath: toLeft_cons_inl, disjUnion_singleton, attach_cons, dens_cons, singleton_disjUnion, toList_cons, Nat.antidiagonal_succ_succ', mem_cons_of_mem, monotone_iff_forall_le_cons, cons_subset_cons, sum_cons, Colex.cons_lt_cons, sum_cons', Int.univ_addEquiv, Nat.antidiagonal_succ, mk_cons, coe_cons, Finsupp.support_add_single, prod_cons', pairwise_cons', cons_nonempty, Fin.univ_succAbove, covBy_iff_exists_cons, fold_cons, erase_cons, toLeft_cons_inr, Nonempty.exists_cons_eq, cons_val, Mathlib.Meta.Finset.insert_eq_cons, Ioc_eq_cons_Ioo, subset_cons, covBy_cons, Icc_eq_cons_Ioc, pairwise_cons, toRight_cons_inl, Iic_eq_cons_Iio, Nat.cons_self_properDivisors, Fin.univ_succ, sym2_cons, Nat.multinomial_cons, inf'_cons, piAntidiag_cons, Finsupp.support_single_add, ssubset_iff_exists_cons_subset, Mathlib.Meta.Finset.range_succ', filter_cons, card_eq_succ_iff_cons, map_cons, Ici_eq_cons_Ioi, sort_cons, prod_powerset_cons, cons_eq_insert, card_cons, toRight_cons_inr, prod_cons, cons_empty, sup_cons, sup'_cons, Icc_eq_cons_Ico, Ico_eq_cons_Ioo, erase_cons_of_ne, Nontrivial.exists_cons_eq, filter_cons_of_pos, strictMono_iff_forall_lt_cons, Fin.univ_castSuccEmb, cons_sdiff_cons, Colex.cons_le_cons, strictAnti_iff_forall_cons_lt, SimpleGraph.edgeFinset_sup_edge, CovBy.exists_finset_cons, sum_powerset_cons, mem_cons, mem_cons_self, inf_cons, filter_cons_of_neg, antitone_iff_forall_cons_le, cons_subset, ssubset_cons, Nat.antidiagonal_succ'
|
consPiProd π | CompOp | 2 mathmath: consPiProd_fst, consPiProd_snd
|
consPiProdEquiv π | CompOp | β |
insertPiProd π | CompOp | 2 mathmath: insertPiProd_snd, insertPiProd_fst
|
insertPiProdEquiv π | CompOp | β |
instInsert π | CompOp | 368 mathmath: insert_Ico_succ_left_eq_Ico, insert_compl_self, insert_val, insert_Ico_left_eq_Ico_pred, collapse_eq, MeasureTheory.SimpleFunc.range_indicator, toList_insert, piecewise_insert, insert_inter_of_notMem, disjoint_insert_erase, pair_comm, SSet.hornββ.desc.multicofork_Ο_two, Nat.binomial_succ_succ, insert_Ico_add_one_left_eq_Ico, Lagrange.basis_pair_right, Polynomial.support_trinomial, weightedVSubOfPoint_insert, neg_insert, set_biUnion_insert_update, SimpleGraph.Dart.edge_fiber, insert_eq, disjoint_erase_insert, sdiff_insert_insert_of_mem_of_notMem, Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, prod_insert, insert_subset_insert, Icc_succ_succ, insert_Icc_left_eq_Icc_sub_one, Nat.filter_range_nth_subset_insert, Finsupp.support_single_add_single, sup_insert, range_add_one', insert_Ioc_right_eq_Ioc_add_one, Nat.factoredNumbers_insert, insert_compl_insert, insert_Ico_right_eq_Ico_add_one_of_not_isMax, Ioi_insert, Fin.orderIsoTriple_zero, Lagrange.interpolate_eq_sum_interpolate_insert_sdiff, coe_eq_pair, mem_insert_self, Multiset.toFinset_cons, sum_pair, SSet.hornββ.desc.multicofork_Ο_one, powerset_insert, antitone_iff_forall_insert_le, compl_erase, Lagrange.nodal_insert_eq_nodal, set_biInter_insert_update, insert_sdiff_self_of_mem, insert_def, Nat.filter_range_nth_eq_insert_of_finite, Set.Finite.toFinset_insert', Equiv.Perm.IsThreeCycle.support_eq_iff_mem_support, subset_insert_iff_of_notMem, range_succ, mem_finsuppAntidiag_insert, SimpleGraph.IsFiveWheelLike.isNClique_right, Fin.orderIsoPair_zero, monotone_iff_forall_le_insert, SSet.hornββ.sq, Turing.TM2to1.trStmtsβ_run, insert_eq_self, insertNone_eraseNone, insert_empty, piAntidiag_insert, attach_insert, Equiv.Perm.support_swap_mul_swap, sum_insert_of_eq_zero_if_notMem, insert_inj_on, insert_subset_iff, Polynomial.support_trinomial', iInf_insert, Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub, insert_subset, SSet.hornββ.desc.multicofork_pt, max_pair, insert_val_of_notMem, insert_Icc_right_eq_Icc_succ, univ_of_card_le_three, insert_Ico_left_eq_Ico_sub_one_of_not_isMin, prod_pair, imageβ_insert_left, insert_Ico_left_eq_Ico_pred_of_not_isMin, Fintype.IsSimpleOrder.univ, insert_sdiff_insert, insert_Ico_sub_one_right_eq_Ico, SimpleGraph.TripartiteFromTriangles.graph_triple, Finpartition.extend_parts, prod_insert', coe_pair, mem_insert_coe, centerMass_insert, insert_sdiff_of_mem, max'_pair, Ico_insert_right, Polynomial.support_binomial', card_add_card_subsetSum_lt_card_subsetSum_insert_max, nonMemberSubfamily_image_insert, Int.divisorsAntidiagonal_three, covBy_iff_exists_insert, insert_inter_of_mem, Finpartition.parts_extendOfLE_of_lt, Equiv.Perm.support_swap_iff, sum_insert_sub, Mathlib.Meta.Finset.insert_eq_cons, UnitsInt.univ, exists_mem_insert, SSet.hornββ.desc.multicofork_Ο_two_assoc, Affine.Simplex.mongePlane_def, card_le_three, SSet.hornββ.desc.multicofork_Ο_zero_assoc, insert_Ioc_succ_left_eq_Ioc, card_le_five, insert_sdiff_of_notMem, SimpleGraph.IsNClique.insert_erase, insert_Ioc_right_eq_Ioc_succ_of_not_isMax, insert_union, map_insert, sdiff_insert, max_mem_insert_bot_image_coe, Int.divisorsAntidiagonal_four, MeasureTheory.lmarginal_insert, insert_Ioc_pred_right_eq_Ioc, sup'_insert, Order.exists_orderEmbedding_insert, sdiff_erase, SimpleGraph.IsFiveWheelLike.isNClique_snd_right, Sym2.toFinset_mk_eq, Fin.orderIsoTriple_one, Affine.Simplex.mem_interior_face_iff_sbtw, range_add_one, mem_insert, Ioc_succ_succ, Finsupp.support_update_ne_zero, card_le_four, insert_erase_invOn, insert_Ioc_right_eq_Ioc_succ, SSet.hornββ.sq, compl_insert, insert_val', set_biInter_insert, IsAddKleinFour.eq_finset_univ, card_eq_two, erase_insert_subset, univ_fin2, union_insert, vadd_finset_subsetSum_subset_subsetSum_insert, card_insert_le, Nat.binomial_one, DFinsupp.support_update_ne_zero, memberSubfamily_image_insert, Affine.Simplex.mem_closedInterior_face_iff_wbtw, singleton_union, erase_ssubset_insert, max'_insert, toRight_insert_inr, Set.toFinset_insert, card_insert_of_notMem, inf_insert, insert_Ioc_left_eq_Ioc_pred_of_not_isMin, disjoint_insert_right, Ico_succ_succ, card_le_two, card_eq_four, Finsupp.support_update, insert_Icc_right_eq_Icc_add_one, erase_insert_of_ne, Colex.insert_le_insert, DFinsupp.support_update, mem_shadow_iff_insert_mem, SimpleGraph.IsFiveWheelLike.exists_isFiveWheelLike_succ_of_not_adj_le_two, inv_insert, erase_eq_iff_eq_insert, supIndep_pair, ssubset_iff, Equiv.Perm.support_swap_mul_ge_support_diff, erase_insert, fold_insert_idem, insert_Icc_succ_left_eq_Icc, strictMono_iff_forall_lt_insert, SimpleGraph.cycleGraph_neighborFinset, biUnion_insert, sum_insert', SimpleGraph.IsFiveWheelLike.isNClique_left, SimpleGraph.is3Clique_iff, min_pair, sym_fill_mem, insert_Icc_add_one_left_eq_Icc, min'_insert, Finsupp.support_single_add_single_subset, offDiag_insert, mem_insert_of_mem, vadd_finset_insert, instLawfulSingleton, insert_union_comm, Nat.pow_mul_mem_factoredNumbers, insert_Icc_pred_right_eq_Icc, iSup_insert, insert_Ico_right_eq_Ico_add_one, iInf_insert_update, Nat.primesBelow_succ, card_insert_eq_ite, Nat.equivProdNatFactoredNumbers_apply, Nat.multinomial_insert_one, prod_insert_one, sum_powerset_insert, BoxIntegral.Prepartition.splitMany_insert, piecewise_insert_of_ne, SupIndep.insert, Fintype.univ_Prop, SSet.hornββ.desc.multicofork_Ο_zero_assoc, erase_insert_eq_erase, Ioo_insert_right, card_pair_eq_one_or_two, gcd_insert, Nat.Prime.divisors, Ioc_insert_left, Int.Icc_eq_pair, Int.divisorsAntidiagonal_two, sort_insert, Finsupp.support_update_subset, Int.divisorsAntidiagonal_one, Icc_diff_both, insert_union_distrib, min'_pair, cons_eq_insert, Nat.Ico_succ_right_eq_insert_Ico, inter_insert_of_notMem, max_insert, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, Polynomial.support_update, card_le_six, filter_insert, insert_Ioc_left_eq_Ioc_sub_one, insert_inter_distrib, SSet.horn.multicoequalizerDiagram, Icc_diff_Ioo_self, insert_sdiff_cancel, SSet.hornββ.desc.multicofork_Ο_three_assoc, covBy_insert, Affine.Simplex.closedInterior_face_eq_affineSegment, card_insert_of_mem, SSet.hornββ.desc.multicofork_Ο_zero, disjoint_insert_left, sym2_insert, card_eq_succ, smul_finset_insert, insert_eq_of_mem, iSup_insert_update, SimpleGraph.IsFiveWheelLike.isNClique_fst_left, insert_nonempty, centerMass_pair, sum_insert_zero, subset_insert, Nat.multinomial_insert, inter_insert, image_insert_memberSubfamily, insert_Ico_right_eq_Ico_succ, SSet.hornββ.desc.multicofork_Ο_three, Ioo_succ_succ, insert_Ioc_sub_one_right_eq_Ioc, SimpleGraph.exists_of_maximal_cliqueFree_not_adj, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, Polynomial.support_update_ne_zero, centroid_pair, Finsupp.cons_support, symInsertEquiv_apply_snd_coe, min_insert, SimpleGraph.IsNClique.insert, jacobiSum_eq_sum_sdiff, insert_Ioc_left_eq_Ioc_pred, Turing.PartrecToTM2.supports_insert, Polynomial.support_binomial, Iio_insert, ssubset_insert, Equiv.Perm.support_swap, Ioo_insert_left, List.toFinset_cons, toLeft_insert_inr, Fintype.univ_bool, insert_idem, symInsertEquiv_apply_fst, SSet.hornββ.desc.multicofork_pt, SimpleGraph.is3Clique_triple_iff, Nat.equivProdNatFactoredNumbers_apply', prod_insert_div, Nat.Prime.divisors_sq, Polynomial.trinomial_support, mem_memberSubfamily, finsuppAntidiag_insert, diag_insert, card_pair, exists_eq_insert_iff, insert_Icc_sub_one_right_eq_Icc, Nat.insert_self_properDivisors, symInsertEquiv_symm_apply_coe, imageβ_insert_right, SkewMonoidAlgebra.support_update, insert_inj, pair_eq_singleton, sum_insert, union_singleton, SimpleGraph.cycleGraph_degree_two_le, Fin.orderIsoTriple_two, Nat.binomial_spec, insert_Ico_pred_right_eq_Ico, lcm_insert, card_eq_three, insert_Icc_left_eq_Icc_pred, insert_subset_insert_iff, mem_upShadow_iff, coe_insert, insert_mem_upShadow, toRight_insert_inl, maximal_iff_forall_insert, insert_erase, set_biUnion_insert, Nat.filter_range_nth_eq_insert_of_infinite, insert_Ico_left_eq_Ico_sub_one, insert_Ico_right_eq_Ico_succ_of_not_isMax, insert_erase_subset, pairwiseDisjoint_pair_insert, SSet.hornββ.desc.multicofork_Ο_zero, SSet.hornββ.desc.multicofork_Ο_three_assoc, Nat.succ_mul_binomial, prod_insert_of_eq_one_if_notMem, SSet.hornββ.desc.multicofork_Ο_one_assoc, inter_insert_of_mem, fold_insert, SimpleGraph.TripartiteFromTriangles.toTriangle_apply, sdiff_insert_of_notMem, powersetCard_succ_insert, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, toLeft_insert_inl, insert_sdiff_insert', insert_comm, univ_of_card_le_two, SSet.hornββ.desc.multicofork_Ο_three, insert_Ioc_add_one_left_eq_Ioc, Nat.filter_range_nth_eq_insert, Nat.binomial_eq_choose, prod_powerset_insert, SSet.hornββ.sq, Lagrange.basis_pair_left, Nat.binomial_eq, inf'_insert, Down.mem_compression, SignType.univ_eq, pi_insert, wcovBy_insert, insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin, strictAnti_iff_forall_lt_insert, Colex.insert_lt_insert, image_insert, piecewise_insert_self, instNonemptyElemCoeInsert, Set.Finite.toFinset_insert, Fin.orderIsoPair_one, IsKleinFour.eq_finset_univ, insert_Ioc_right_eq_Ioc_add_one_of_not_isMax, MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton, subset_insert_iff, MeasureTheory.lmarginal_insert', min_mem_insert_top_image_coe, insert_inj_on', CovBy.exists_finset_insert, insert_inter
|
instSingleton π | CompOp | 581 mathmath: Polynomial.support_monomial, Function.update_eq_updateFinset, coe_eq_singleton, notMem_singleton, pairwiseDisjoint_singleton_iff_injOn, Colex.toColex_le_singleton, insert_compl_self, MvPolynomial.vars_X, MeasureTheory.SimpleFunc.range_indicator, sup_singleton_eq_self, pair_comm, Affine.Simplex.sSameSide_excenter_singleton_point, powerset_eq_singleton_empty, preimage_add_left_singleton, imageβ_inter_singleton, map_zero, singletonAddMonoidHom_apply, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_isLimit_lift, SSet.hornββ.desc.multicofork_Ο_two, Nat.binomial_succ_succ, noncommSum_singleton, Ioi_disjUnion_Iio, mem_singleton, Lagrange.basis_pair_right, singleton_pow, singleton_sub, max'_singleton, piAntidiag_zero, Finsupp.single_eq_indicator, Polynomial.support_trinomial, isAddUnit_iff, preimage_mul_left_one, Nat.Ioc_succ_singleton, SSet.horn.faceSingletonComplIso_inv_ΞΉ_assoc, Affine.Simplex.sign_excenterWeights_singleton_pos, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ΞΉ_eq_Ξ΄, Nonempty.eq_singleton_default, Affine.Simplex.excenter_singleton_mem_affineSpan_range, pairwiseDisjoint_range_singleton, Polynomial.support_C_mul_X, mem_singleton_self, disjiUnion_singleton_eq_self, sdiff_singleton_eq_erase, isAtom_iff, SimpleGraph.Dart.edge_fiber, SimpleGraph.isNClique_singleton, insert_eq, product_singleton, Fin.image_succ_univ, MvPolynomial.support_monomial, coe_singleton, Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub, singleton_zpow, Affine.Triangle.sbtw_touchpoint_singleton, Icc_succ_succ, Finsupp.support_single_add_single, imageβ_left_identity, singleton_val, Polynomial.coeffs_monomial, Fin.orderIsoTriple_zero, Equiv.Perm.cycleFactorsFinset_mul_inv_mem_eq_sdiff, coe_eq_pair, BoxIntegral.Prepartition.top_boxes, sum_pair, falling_zero_subset, image_const, SSet.hornββ.desc.multicofork_Ο_one, card_eq_one, vadd_finset_singleton, disjSups_singleton, Matrix.adjp_apply, ssubset_singleton_iff, Nat.antidiagonalTuple_one, singleton_vsub_singleton, prod_singleton, Finsupp.eq_single_iff, preimage_mul_left_singleton, add_singleton, insert_sdiff_self_of_mem, Finpartition.parts_bot, Lagrange.basis_singleton, max_singleton, singletonMonoidHom_apply, Affine.Simplex.excenter_singleton_injective, card_imageβ_singleton_left, Equiv.Perm.IsThreeCycle.support_eq_iff_mem_support, Int.univ_addEquiv, Fin.orderIsoSingleton_apply, sup_singleton, Polynomial.support_C_mul_X', Affine.Simplex.touchpoint_singleton_mem_interior_faceOpposite, Function.update_updateFinset, singleton_diffs_singleton, Fin.orderIsoPair_zero, pairwise_coprime_iff_coprime_prod, SSet.hornββ.sq, inter_singleton_of_mem, MvPolynomial.coeffs_one, Turing.TM2to1.trStmtsβ_run, Equiv.Perm.support_swap_mul_eq, Ico_filter_le_left, not_nontrivial_singleton, MvPolynomial.coeffs_one_of_nontrivial, Nat.Prime.properDivisors, insert_empty, singleton_subset_set_iff, Equiv.Perm.support_swap_mul_swap, erase_eq, compl_singleton, Polynomial.support_trinomial', singleton_mul, singleton_product_singleton, piAntidiag_empty, lcm_singleton, SimpleGraph.neighborFinset_completeEquipartiteGraph, DirectSum.support_of, preimage_add_left_zero, Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub, SSet.hornββ.desc.multicofork_pt, Equiv.Perm.IsCycle.cycleFactorsFinset_eq_singleton, SimpleGraph.neighborFinset_compl, MvPolynomial.coeffs_C, inv_singleton, Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff, max_pair, univ_of_card_le_three, iSup_singleton, Affine.Triangle.excenter_eq_incenter_or_excenter_singleton_of_ne, singleton_eq_univ, prod_pair, SSet.horn.faceSingletonComplIso_inv_ΞΉ, eraseNone_none, SimpleGraph.neighborFinset_disjoint_singleton, preimage_mul_right_one', Fintype.IsSimpleOrder.univ, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_isColimit_desc, antidiagonal_zero, Colex.singleton_le_toColex, smul_singleton, Icc_diff_Ioc_self, SimpleGraph.TripartiteFromTriangles.graph_triple, SimpleGraph.edgeFinset_replaceVertex_of_adj, Nat.antidiagonalTuple_zero_right, eq_singleton_iff_nonempty_unique_mem, singleton_sups_singleton, prod_eq_prod_diff_singleton_mul, smul_finset_singleton, Finpartition.indiscrete_parts, Affine.Triangle.touchpoint_singleton_sbtw, Affine.Simplex.face_eq_mkOfPoint, Fintype.piFinset_update_singleton_eq_filter_piFinset_eq, card_le_one_iff_subset_singleton, Function.updateFinset_singleton, FreeAbelianGroup.support_of, offDiag_singleton, Part.toFinset_some, sups_singleton, card_singleton_inter, coe_pair, SSet.stdSimplex.range_Ξ΄, SimpleGraph.isUniform_singleton, set_biUnion_singleton, filter_fst_eq_antidiagonal, singleton_diffs, max'_pair, Polynomial.support_binomial', Finpartition.parts_top_subset, sup'_singleton, fold_singleton, coe_singletonAddMonoidHom, erase_eq_empty_iff, map_one, Polynomial.support_C, Nat.antidiagonalTuple_zero_zero, smulAntidiagonal_min_smul_min, coe_singletonMulHom, Int.divisorsAntidiagonal_three, Nat.antidiagonal_zero, Option.toFinset_some, image_zero, coe_singletonOneHom, neg_singleton, pure_def, subset_compl_singleton, singleton_infs, singleton_nonempty, range_filter_eq, SSet.stdSimplex.faceSingletonIso_zero_hom_comp_ΞΉ_eq_Ξ΄_assoc, sum_eq_sum_diff_singleton_add, Equiv.Perm.support_swap_iff, UnitsInt.univ, SSet.hornββ.desc.multicofork_Ο_two_assoc, update_eq_piecewise, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone_cocone_ΞΉ_app, Finsupp.frange_single, Affine.Simplex.mongePlane_def, card_le_three, singleton_subset_iff, SSet.hornββ.desc.multicofork_Ο_zero_assoc, Fintype.prod_eq_prod_compl_mul, card_le_five, isCoatom_compl_singleton, card_imageβ_singleton_right, SimpleGraph.neighborFinset_boxProd, singleton_inter_of_notMem, univ_unique, Ioc_diff_Ioo_self, singleton_biUnion, Turing.PartrecToTM2.supports_singleton, Affine.Simplex.sign_excenterWeights_singleton_neg, Int.divisorsAntidiagonal_four, singleton_smul, MeasureTheory.lmarginal_singleton, singleton_injective, Finsupp.support_single_ne_zero, Affine.Simplex.sum_excenterWeightsUnnorm_singleton_pos, Iic_bot, exists_sum_eq_one_iff_pairwise_coprime', Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point, truncatedSup_singleton, Sym2.toFinset_mk_eq, singleton_vadd_singleton, MeasureTheory.SimpleFunc.range_zero, Fin.orderIsoTriple_one, image_singleton, Affine.Simplex.mem_interior_face_iff_sbtw, Ioc_succ_succ, card_le_four, SSet.hornββ.sq, Finsupp.support_subset_singleton, singleton_subset_coe, Fintype.prod_eq_mul_prod_compl, Polynomial.support_C_subset, fold_union_empty_singleton, Polynomial.support_C_mul_X_pow', Nat.finMulAntidiag_one, addAntidiagonal_min_add_min, Polynomial.support_X, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ΞΉ_eq_Ξ΄, singleton_mul_inter, orderEmbOfFin_singleton, Fintype.univ_unit, IsAddKleinFour.eq_finset_univ, card_eq_two, filter_eq', univ_fin2, Shatters.exists_inter_eq_singleton, SSet.stdSimplex.faceSingletonComplIso_hom_ΞΉ, Nat.binomial_one, Affine.Triangle.excenter_eq_incenter_or_excenter_singleton, preimage_mul_right_one, Affine.Simplex.mem_closedInterior_face_iff_wbtw, singleton_union, sym_zero, pi_const_singleton, Colex.toColex_lt_singleton, AddAction.stabilizer_finset_singleton, Affine.Simplex.exradius_singleton_pos, singleton_sub_singleton, IsUnit.finset, Colex.singleton_lt_singleton, eq_singleton_iff_unique_mem, zsmul_singleton, singleton_add_inter, Ico_succ_succ, fold_sup_bot_singleton, Finsupp.support_eq_singleton, Equiv.Perm.cycleFactorsFinset_eq_singleton_iff, card_le_two, Set.toFinset_singleton, sub_singleton, filter_snd_eq_antidiagonal, MvPolynomial.support_esymm', card_eq_four, disjiUnion_singleton, Nat.properDivisors_eq_singleton_one_iff_prime, addRothNumber_singleton, eq_singleton_or_nontrivial, prod_prod_Ioi_mul_eq_prod_prod_off_diag, Affine.Simplex.sOppSide_excenter_singleton_point, sum_singleton, Nat.Ico_pred_singleton, default_singleton, singleton_add, Finmap.keys_singleton, MulAction.stabilizer_finset_singleton, SSet.face_le_horn, add_eq_zero_iff, Icc_eq_singleton_iff, singleton_add_singleton, truncatedInf_singleton, orderEmbOfFin_compl_singleton_eq_succAboveOrderEmb, singleton_zero, Nontrivial.not_subset_singleton, supIndep_pair, Equiv.Perm.support_swap_mul_ge_support_diff, Finpartition.mem_bot_iff, biUnion_singleton_eq_self, SSet.horn.faceΞΉ_ΞΉ, SimpleGraph.cycleGraph_neighborFinset, FreeAddMonoid.symbols_of, shadow_singleton, supIndep_singleton, shadow_singleton_empty, singleton_infs_singleton, Affine.Simplex.sign_touchpointWeights_singleton_pos, singleton_inter_of_mem, SimpleGraph.is3Clique_iff, min_pair, Fin.image_castSucc, singletonAddHom_apply, erase_sdiff_erase, Geometry.SimplicialComplex.mem_vertices, Finsupp.support_single_add_single_subset, offDiag_insert, instLawfulSingleton, SSet.horn_eq_iSup, Multiset.toFinset_replicate, sym_singleton, inter_singleton_of_notMem, gcd_singleton, singleton_mul_singleton, Polynomial.coeffs_one, disjoint_singleton, singleton_inj, SimpleGraph.isNClique_one, FreeMonoid.symbols_of, sup_singleton_apply, Affine.Simplex.sOppSide_point_excenter_singleton, Finsupp.antidiagonal_zero, MvPolynomial.support_monomial_subset, SimpleGraph.sdiff_compl_neighborFinset_inter_eq, prod_singleton', inter_singleton, MvPolynomial.support_X_pow, isAtom_singleton, Fintype.univ_Prop, Nat.multinomial_singleton, Affine.Simplex.sign_touchpointWeights_singleton_neg, iInf_singleton, SSet.hornββ.desc.multicofork_Ο_zero_assoc, sum_sum_Ioi_add_eq_sum_sum_off_diag, pi_empty, BoxIntegral.Prepartition.single_boxes, YoungDiagram.row_eq_prod, imageβ_singleton_left, min'_singleton, card_pair_eq_one_or_two, Fintype.sum_eq_sum_compl_add, SkewMonoidAlgebra.support_single_subset, card_add_singleton, AddMonoidAlgebra.mem_grade_iff, Finsupp.rangeSingleton_apply, Nat.Prime.divisors, SSet.horn.faceΞΉ_ΞΉ_assoc, preimage_add_right_singleton, Int.Icc_eq_pair, Int.divisorsAntidiagonal_two, List.fixedLengthDigits_zero, sum_update_of_mem, Icc_diff_Ico_self, Int.divisorsAntidiagonal_one, inter_add_singleton, Icc_diff_both, IsLocalRing.primesOverFinset_eq, piAntidiag_empty_zero, Icc_self, centroid_singleton, piecewise_singleton, IsPrimitiveRoot.primitiveRoots_one, infs_singleton, min'_pair, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, card_le_six, isUnit_iff_singleton, univ_eq_singleton_of_card_one, Polynomial.support_C_mul_X_pow, dens_singleton, isUnit_singleton, SSet.horn.multicoequalizerDiagram, finsuppAntidiag_empty_zero, Icc_diff_Ioo_self, insert_sdiff_cancel, singleton_vsub, sum_eq_add_sum_diff_singleton, SSet.hornββ.desc.multicofork_Ο_three_assoc, MeasureTheory.SimpleFunc.range_one, finsuppAntidiag_empty, Affine.Simplex.closedInterior_face_eq_affineSegment, SSet.hornββ.desc.multicofork_Ο_zero, empty_covBy_singleton, MeasureTheory.SimpleFunc.range_const, Set.Finite.toFinset_singleton, DirectSum.support_of_subset, map_singleton, Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton, div_singleton, SSet.stdSimplex.ofSimplex_yonedaEquiv_Ξ΄, nonempty_iff_eq_singleton_default, card_singleton_add, min_singleton, sum_singleton', centerMass_pair, Finsupp.support_subset_singleton', Affine.Simplex.touchpointWeights_singleton_neg, diffs_singleton, subset_singleton_iff, Polynomial.support_X_pow, preimage_mul_left_one', cons_empty, SSet.hornββ.desc.multicofork_Ο_three, nsmul_singleton, Ioo_succ_succ, mulAntidiagonal_min_mul_min, subset_singleton_iff', Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, centroid_pair, DFinsupp.support_single_subset, imageβ_singleton_left', range_sdiff_zero, imageβ_singleton_right, AhlswedeZhang.supSum_singleton, CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone_cone_Ο_app, SSet.stdSimplex.faceSingletonComplIso_hom_ΞΉ_assoc, Fintype.piFinset_singleton, prod_eq_mul_prod_diff_singleton, Filter.atTop_finset_eq_iInf, singleton_subset_singleton, powersetCard_zero, sdiff_erase_self, jacobiSum_eq_sum_sdiff, Polynomial.support_binomial, Colex.singleton_le_singleton, LaurentPolynomial.support_C_mul_T_of_ne_zero, empty_ssubset_singleton, Equiv.Perm.support_swap, SSet.boundary_eq_iSup, Ico_diff_Ioo_self, Nat.Ico_succ_singleton, Affine.Simplex.sSameSide_point_excenter_singleton, disjoint_singleton_right, Nontrivial.sdiff_singleton_nonempty, inf_singleton, Fintype.univ_bool, singleton_inter, Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton, disjoint_singleton_left, Finsupp.support_single_subset, isCoatom_iff, Affine.Simplex.touchpointWeights_singleton_pos, SSet.hornββ.desc.multicofork_pt, SimpleGraph.is3Clique_triple_iff, Nat.Prime.divisors_sq, range_one, singleton_sups, Polynomial.trinomial_support, cons_sdiff_cons, coe_singletonAddHom, inf'_singleton, YoungDiagram.col_eq_prod, biUnion_singleton, singletonMulHom_apply, Fintype.univ_punit, powerset_empty, card_pair, card_mul_singleton, isAddUnit_singleton, MeasureTheory.SimpleFunc.range_const_subset, singleton_product, Nonempty.subset_singleton_iff, SimpleGraph.compl_neighborFinset_sdiff_inter_eq, isUnit_iff, Tree.treesOfNumNodesEq_zero, SSet.stdSimplex.faceSingletonIso_one_hom_comp_ΞΉ_eq_Ξ΄_assoc, set_biInter_singleton, toList_eq_singleton_iff, exists_sum_eq_one_iff_pairwise_coprime, IsAddUnit.finset, box_zero, filter_singleton, pair_eq_singleton, LaurentPolynomial.support_C_mul_T, preimage_add_left_zero', pairwise_isRelPrime_iff_isRelPrime_prod, union_singleton, Nat.divisorsAntidiagonal_one, Nat.divisors_one, SimpleGraph.cycleGraph_degree_two_le, Fin.orderIsoTriple_two, Nat.binomial_spec, List.toFinset_replicate_of_ne_zero, finsuppAntidiag_zero, MvPolynomial.coeffs_C_subset, uIcc_self, preimage_add_right_zero, singletonOneHom_apply, card_eq_three, Nat.Prime.primeFactors, Polynomial.support_monomial', vaddAntidiagonal_min_vadd_min, image_one, Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point, vadd_singleton, inter_mul_singleton, Fintype.sum_eq_add_sum_compl, Fin.image_succAbove_univ, noncommProd_singleton, diag_singleton, singletonZeroHom_apply, Nat.primeFactors_prime_pow, singleton_one, DFinsupp.support_single_ne_zero, mul_eq_one_iff, Affine.Simplex.excenterExists_singleton, Fintype.univ_ofSubsingleton, preimage_mul_right_singleton, SSet.hornββ.desc.multicofork_Ο_zero, SSet.hornββ.desc.multicofork_Ο_three_assoc, isUnit_iff_singleton_aux, Nat.succ_mul_binomial, SSet.hornββ.desc.multicofork_Ο_one_assoc, SimpleGraph.singleton_disjoint_neighborFinset, Nonempty.exists_eq_singleton_or_nontrivial, SimpleGraph.TripartiteFromTriangles.toTriangle_apply, expect_singleton, singleton_iff_unique_mem, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, singleton_div_singleton, erase_singleton, powersetCard_one, preimage_add_right_zero', MvPolynomial.support_X, insert_sdiff_insert', Multiset.toFinset_singleton, imageβ_right_identity, pi_singletons, univ_of_card_le_two, card_singleton_mul, SSet.hornββ.desc.multicofork_Ο_three, sort_singleton, prod_update_of_mem, Nat.binomial_eq_choose, SSet.hornββ.sq, Lagrange.basis_pair_left, Nat.binomial_eq, Finsupp.support_eq_singleton', imageβ_singleton_inter, SignType.univ_eq, Affine.Simplex.faceOppositeCentroid_eq_affineCombination, mul_singleton, vsub_singleton, MvPolynomial.support_C, Multiset.toEnumFinset_filter_eq, singleton_smul_singleton, coe_subset_singleton, Ici_top, centerMass_singleton, SimpleGraph.cliqueSet_one, compls_singleton, SSet.stdSimplex.face_singleton_compl, coe_singletonZeroHom, filter_eq, Lagrange.interpolate_singleton, MvPolynomial.vars_monomial_single, Fin.orderIsoPair_one, IsKleinFour.eq_finset_univ, singleton_vadd, MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton, imageβ_singleton, singleton_div, powersetCard_self, mulRothNumber_singleton, toList_singleton, sym2_singleton, Finpartition.atomise_empty, val_eq_singleton_iff, card_singleton, Multiset.toFinset_eq_singleton_iff, coe_singletonMonoidHom, SkewMonoidAlgebra.support_single_ne_zero, Polynomial.toSubring_one
|
instUniqueOfIsEmpty π | CompOp | β |
instUniqueSubtypeMemSingleton π | CompOp | 3 mathmath: Function.update_eq_updateFinset, Function.update_updateFinset, default_singleton
|
prodPiCons π | CompOp | β |
prodPiInsert π | CompOp | β |
subtypeInsertEquivOption π | CompOp | β |