| Name | Category | Theorems |
|---|
toDecidableEq π | CompOp | 158 mathmath: Finset.insert_Ico_succ_left_eq_Ico, Multiset.Ico_sub_Ico_right, WithLp.prod_edist_eq_card, Finset.min'_union, Finset.insert_Ico_left_eq_Ico_pred, Finset.max_union, Multiset.Ico_sub_Ico_left, Finset.insert_Ico_add_one_left_eq_Ico, Finset.Ioi_disjUnion_Iio, ProbabilityTheory.Kernel.borelMarkovFromReal_apply', Finset.Ico_subset_Ico_union_Ico, Finset.image_orderEmbOfFin_univ, Finset.uIcc_eq_union, DFinsupp.disjoint_iff, Finset.Ioc_union_Ioc_eq_Ioc, Finset.insert_Icc_left_eq_Icc_sub_one, Finset.insert_Ioc_right_eq_Ioc_add_one, Finset.map_ofDual_max, Finset.Colex.toColex_lt_toColex_iff_max'_mem, Finset.insert_Ico_right_eq_Ico_add_one_of_not_isMax, Finset.min_union, Finset.Colex.le_iff_max'_mem, Finset.orderIsoOfFin_symm_apply, MultilinearMap.map_piecewise_sub_map_piecewise, Finset.Ico_diff_Ico_left, Profinite.NobelingProof.fin_comap_jointlySurjective, Finset.Colex.toColex_le_toColex_iff_max'_mem, Finset.Ico_union_Ico', Finset.toDual_min', Pi.toLex_update_le_self_iff, Finset.Iic_union_Ioc_eq_Iic, Pi.toLex_update_lt_self_iff, Profinite.NobelingProof.GoodProducts.spanFin, Finset.max_pair, Finset.insert_Icc_right_eq_Icc_succ, Finset.insert_Ico_left_eq_Ico_sub_one_of_not_isMin, Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin, Finset.insert_Ico_sub_one_right_eq_Ico, Finset.Colex.toColex_image_lt_toColex_image, Order.krullDim_le_of_krullDim_preimage_le, Pi.le_toLex_update_self_iff, Finset.max'_pair, OrderIso.withZeroUnits_symm_apply, QuadraticMap.toBilin_apply, Finset.map_toDual_max, Finset.max_mem_image_coe, Finset.Ico_inter_Ico, ENNReal.mul_rpow_eq_ite, Finset.Nonempty.ciSup_mem_image, WithZero.withZeroUnitsEquiv_symm_strictMono, HomogeneousIdeal.coe_radical, Finset.insert_Ioc_succ_left_eq_Ioc, Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax, DFinsupp.support_inf, Finset.max_mem_insert_bot_image_coe, Finset.Ioc_inter_Ioc, Finset.insert_Ioc_pred_right_eq_Ioc, Order.exists_orderEmbedding_insert, Finset.insert_Ioc_right_eq_Ioc_succ, Monotone.map_finset_min', toZ_of_ge, ENNReal.mul_top', Multiset.map_count_True_eq_filter_card, Profinite.NobelingProof.factors_prod_eq_basis_of_ne, Finset.Colex.lt_iff_exists_filter_lt, Finset.map_toDual_min, ENat.mul_top', instLawfulBCmpCompare_mathlib, Finset.min_mem_image_coe, Finset.Ico_union_Ico_eq_Ico, Finset.max'_insert, Pi.lt_toColex_update_self_iff, MeasureTheory.stoppedValue_stoppedProcess, Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin, Finset.ciInf_mem_image, Multiset.Ico_inter_Ico, Finset.insert_Icc_right_eq_Icc_add_one, Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag, Finset.toDual_max', Finset.Ico_union_Ico, PMF.toOuterMeasure_bindOnSupport_apply, Finset.insert_Icc_succ_left_eq_Icc, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval, Finset.max'_union, Ideal.IsPrime.homogeneousCore, Finset.min_pair, Finset.Colex.shadow_initSeg, Finset.insert_Icc_add_one_left_eq_Icc, Finset.min'_insert, Profinite.NobelingProof.spanFinBasis.span, Finset.insert_Icc_pred_right_eq_Icc, Finset.insert_Ico_right_eq_Ico_add_one, HahnEmbedding.ArchimedeanStrata.isInternal_stratum', Fintype.univ_Prop, Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag, ENNReal.top_mul', Finset.Colex.IsInitSeg.shadow, ENNReal.coe_rpow_def, Finset.UV.toColex_compress_lt_toColex, Pi.lt_toLex_update_self_iff, Finset.ofDual_min', Polynomial.ringKrullDim_le, Finset.min'_pair, Finset.max_insert, Finset.insert_Ioc_left_eq_Ioc_sub_one, Finset.Colex.lt_iff_max'_mem, Finset.Colex.erase_le_erase_min', cauchy_davenport_mul_of_linearOrder_isCancelMul, ProbabilityTheory.Kernel.borelMarkovFromReal_apply, Pi.toColex_update_le_self_iff, Finset.Ico_diff_Ico_right, cmp_eq_compareOfLessAndEq, Finset.insert_Ico_right_eq_Ico_succ, Finset.insert_Ioc_sub_one_right_eq_Ioc, Finset.Colex.toColex_image_ofColex_strictMono, Finset.card_le_diff_of_interleaved, Finset.min_insert, Finset.insert_Ioc_left_eq_Ioc_pred, Finset.Colex.toColex_image_le_toColex_image, PMF.toMeasure_bindOnSupport_apply, ProbabilityTheory.Kernel.densityProcess_fst_univ, ENNReal.top_div, Monotone.map_finset_max', compare_eq_compareOfLessAndEq, Finset.sum_sym2_filter_not_isDiag, Finset.insert_Icc_sub_one_right_eq_Icc, Pi.le_toColex_update_self_iff, Finset.map_ofDual_min, Finset.insert_Ico_pred_right_eq_Ico, GenContFract.sub_convs_eq, Finset.insert_Icc_left_eq_Icc_pred, MultilinearMap.map_sub_map_piecewise, Finset.insert_Ico_left_eq_Ico_sub_one, LinearOrderedCommGroupWithZero.inl_apply, Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax, LinearOrderedCommGroupWithZero.inr_apply, Finset.uIcc_subset_uIcc_union_uIcc, WithZeroTopology.nhds_eq_update, PMF.bindOnSupport_apply, MeasureTheory.exp_llr, Finset.ofDual_max', Finset.ciSup_mem_image, Finset.Iic_diff_Ioc, Finset.insert_Ioc_add_one_left_eq_Ioc, cauchy_davenport_add_of_linearOrder_isCancelAdd, Order.krullDim_le_of_krullDim_preimage_le', toZ_of_lt, Finset.insert_Ioc_left_eq_Ioc_sub_one_of_not_isMin, Matrix.BlockTriangular.charpoly, Profinite.NobelingProof.factors_prod_eq_basis, Profinite.NobelingProof.factors_prod_eq_basis_of_eq, Finset.Iic_diff_Ioc_self_of_le, Pi.toColex_update_lt_self_iff, WithZero.withZeroUnitsEquiv_strictMono, DFinsupp.support_sup, Finset.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax, ENat.top_mul', Finset.min_mem_insert_top_image_coe
|
toDecidableLE π | CompOp | 36 mathmath: List.sortedLE_mergeSort, Finset.sortedGT_sort, Finset.orderIsoOfFin_symm_apply, PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius, PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, min_def', max_def', List.sortedLE_insertionSort, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, negPart_eq_ite, concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic, Finset.max'_eq_sorted_last, posPart_eq_ite, convexOn_univ_piecewise_Ici_of_monotoneOn_Ici_antitoneOn_Iic, Finset.sort_sorted_lt, min_def, convexOn_univ_piecewise_Iic_of_antitoneOn_Iic_monotoneOn_Ici, max_def, Finset.Ico_filter_le, Finset.min'_eq_sorted_zero, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, Finset.sortedLT_sort, Finset.orderEmbOfFin_apply, Multiset.Ico_filter_le, Finset.sort_sorted_gt, concaveOn_univ_piecewise_Iic_of_monotoneOn_Iic_antitoneOn_Ici, leOnePart_eq_ite, PairReduction.exists_radius_le, List.sortedGE_mergeSort, StrictMonoOn.map_finsetSort, oneLePart_eq_ite, min_def, List.sortedGE_insertionSort, Finset.listMap_orderEmbOfFin_finRange, max_def
|
toDecidableLT π | CompOp | 150 mathmath: Profinite.NobelingProof.GoodProducts.sum_to_range, sign_mul_self, Profinite.NobelingProof.injective_Οs', Finset.prod_one_sub_ordered, List.getD_max?_eq_unbotD_maximum, Finset.Iio_filter_lt, max_def_lt, List.maximum_cons, List.foldr_max_of_ne_nil, Eq.cmp_eq_eq', Ordering.Compares.cmp_eq, signHom_apply, List.minimum_of_length_pos_le_iff, Profinite.NobelingProof.coe_Οs, Profinite.NobelingProof.Products.limitOrdinal, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, Eq.cmp_eq_eq, sign_nonneg_iff, Profinite.NobelingProof.Products.eval_Οs, List.coe_maximum_of_length_pos, MultilinearMap.map_piecewise_sub_map_piecewise, HahnEmbedding.Partial.truncLT_mem_range_extendFun, List.mem_argmin_iff, Profinite.NobelingProof.Products.eval_Οs', Profinite.NobelingProof.GoodProducts.span_sum, cmp_add_left, Profinite.NobelingProof.succ_exact, Profinite.NobelingProof.GoodProducts.smaller_factorization, List.coe_le_maximum_iff, Profinite.NobelingProof.Οs'_apply_apply, StrictAnti.cmp_map_eq, oneLePart_eq_ite_lt, cmp_self_eq_eq, cmp_eq_cmp_symm, List.minimum_append, Finset.prod_sub_ordered, sign_mul_abs, sign_eq_of_affineCombination_mem_affineSpan_single_lineMap, PNat.sub_coe, StrictAntiOn.cmp_map_eq, cmp_mul_pos_left, QuadraticMap.toBilin_apply, LT.lt.cmp_eq_gt, Multiset.Ico_filter_lt, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, Finset.prod_one_add_ordered, HahnEmbedding.IsPartial.truncLT_mem_range, Profinite.NobelingProof.contained_eq_proj, List.argmax_cons, Profinite.NobelingProof.GoodProducts.injective_sum_to, Order.PartialIso.exists_across, leOnePart_eq_ite_lt, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, Profinite.NobelingProof.GoodProducts.good_lt_maxProducts, Profinite.NobelingProof.GoodProducts.union_succ, Finset.prod_add_ordered, abs_mul_sign, Profinite.NobelingProof.Products.eval_Οs_image', cmp_eq_compare, Finset.Colex.lt_iff_exists_filter_lt, LT.lt.cmp_eq_lt, List.minimum_cons, Ordinal.cmp_veblen, List.getD_min?_eq_untopD_minimum, cmp_mul_right', Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, List.minimum_eq_coe_iff, sign_mul, List.le_minimum_of_forall_le, HahnSeries.coeff_truncLT_of_le, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, self_mul_sign, Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one, List.argmax_eq_some_iff, cmp_sub_zero, Profinite.NobelingProof.C0_projOrd, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, Profinite.NobelingProof.C1_projOrd, Profinite.NobelingProof.Οs_apply_apply, StrictMonoOn.cmp_map_eq, cmp_eq_eq_iff, Profinite.NobelingProof.GoodProducts.square_commutes, min_def_lt', MeasureTheory.stoppedProcess_eq_of_mem_finset, List.maximum_le_of_forall_le, Profinite.NobelingProof.contained_C1, Profinite.NobelingProof.isClosed_proj, cmp_mul_pos_right, List.mem_argmax_iff, List.le_maximum_of_mem', Profinite.NobelingProof.swapTrue_mem_C1, sign_nonpos_iff, sign_pow, StrictMono.sign_comp, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, sign_eq_zero_iff, Ordinal.cmp_veblenWith, Finset.Ioo_filter_lt, StrictMono.cmp_map_eq, List.minimum_anti, Profinite.NobelingProof.contained_proj, cmp_eq_compareOfLessAndEq, HahnSeries.SummableFamily.powers_toFun, List.Perm.maximum_eq, List.maximum_mono, List.foldr_min_of_ne_nil, cmp_eq_gt_iff, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, cmp_eq_lt_iff, cmp_mul_left', cmp_compares, Matrix.BlockTriangular.inv_toBlock, sign_eq_sign_or_eq_neg, List.minimum_le_of_mem', Profinite.NobelingProof.CC_comp_zero, min_def_lt, cmp_mul_neg_left, Profinite.NobelingProof.CC_exact, Polynomial.signVariations_eq_eraseLead_add_ite, compare_eq_compareOfLessAndEq, Finset.sum_sym2_filter_not_isDiag, cmp_mul_neg_right, HahnEmbedding.Partial.eval_eq_truncLT, List.minimum_concat, Profinite.NobelingProof.injective_Οs, cmp_div_one', Finset.Ico_filter_lt, List.argmin_eq_some_iff, Profinite.NobelingProof.coe_Οs', Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, MultilinearMap.map_sub_map_piecewise, cmp_add_right, Polynomial.roots_countP_pos_le_signVariations, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, List.minimum_le_coe_iff, continuousAt_sign_of_ne_zero, List.maximum_eq_coe_iff, List.le_maximum_of_length_pos_iff, List.coe_minimum_of_length_pos, max_def_lt', Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, Profinite.NobelingProof.Products.eval_Οs_image, negPart_eq_ite_lt, List.trop_minimum, List.maximum_concat, List.maximum_append, List.argmin_cons, posPart_eq_ite_lt, List.Perm.minimum_eq, Profinite.NobelingProof.succ_mono
|
toMax π | CompOp | 21 mathmath: le_max_right, eq_max, max_def_lt, max_left_comm, max_eq_right_of_lt, max_def', max_rec, PUnit.max_eq, max_self, max_eq_left, max_lt, max_eq_right, max_def, max_le, max_assoc, max_eq_left_of_lt, max_rec', le_max_left, max_def, max_def_lt', max_comm
|
toMin π | CompOp | 23 mathmath: PUnit.min_eq, min_comm, min_rec, min_eq_left_of_lt, min_self, ArchimedeanClass.FiniteElement.mk_add_mk, min_def', lt_min, min_assoc, min_eq_right, le_min, min_le_left, min_def, min_def_lt', min_eq_left, min_eq_right_of_lt, min_le_right, min_left_comm, min_def_lt, min_def, min_rec', eq_min, ArchimedeanClass.FiniteElement.mk_sub_mk
|
toOrd π | CompOp | 8 mathmath: compare_eq_iff_eq, compare_gt_iff_gt, cmp_eq_compare, instLawfulBCmpCompare_mathlib, compare_lt_iff_lt, compare_of_injective_eq_compareOfLessAndEq, compare_eq_compareOfLessAndEq, compare_iff
|
toPartialOrder π | CompOp | 192 mathmath: lt_or_gt_iff_ne', le_max_right, not_le, ofDual_toAdd_zero, LinearOrderedAddCommGroupWithTop.neg_eq_top, LinearOrderedAddCommGroupWithTop.sub_pos, not_monotone_not_antitone_iff_exists_le_le, lt_or_gt_of_ne, lt_iff_not_ge, compl_le, toPartialOrder_injective_iff, instTrichotomousLt, IsWellFounded.wellOrderExtension.isWellFounded_lt, max_def_lt, zpow_right_antiβ, Eq.cmp_eq_eq', addLeftReflectLT_of_addLeftMono, AddValuation.top_iff, addRightStrictMono_of_addRightReflectLE, isWellOrder_lt, zpow_left_injOnβ, Eq.cmp_eq_eq, LinearOrderedAddCommGroupWithTop.add_eq_top, noTopOrder_iff_noMaxOrder, add_top, PUnit.le, inv_le_one_iffβ, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, isWellOrder_gt, gt_trichotomy, instTrichotomousLe, CategoryTheory.TransfiniteCompositionOfShape.ici_F, ContinuousMap.HomotopyRel.trans_apply, one_div_neg, compare_gt_iff_gt, instIsStrictTotalOrderLt, le_iff_le_iff_lt_iff_lt, MulPosReflectLE.toMulPosStrictMono, PNat.not_lt_one, cmp_self_eq_eq, cmp_eq_cmp_symm, ofAdd_bot, Path.Homotopy.hcomp_apply, LinearOrderedAddCommGroupWithTop.sub_top, covariant_le_iff_contravariant_lt, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, MonomialOrder.lex_lt_iff_of_unique, LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid, not_lt_iff_eq_or_lt, covariant_lt_iff_contravariant_le, mulPosStrictMono_iff_mulPosReflectLE, PNat.coe_le_coe, mulRightReflectLT_of_mulRightMono, LinearOrderedAddCommGroupWithTop.neg_pos, min_def', strictMono_int_of_lt_succ, max_def', LinearOrderedAddCommGroupWithTop.top_pos, PosMulReflectLT.toPosMulMono, forall_ge_imp_ne_iff_lt, forall_gt_imp_ge_iff_le_of_dense, mulRightStrictMono_of_mulRightReflectLE, IicProdIoc_def, ContinuousMap.HomotopyWith.trans_apply, compl_ge, LinearOrderedAddCommGroupWithTop.add_lt_top, lt_of_forall_le_imp_ne, cmp_eq_compare, compare_ge_iff_ge, forall_lt_imp_ne_iff_le, inv_neg'', Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator, contravariant_lt_of_covariant_le, AddValuation.map_zero, mulLeftReflectLT_of_mulLeftMono, instLawfulBCmpCompare_mathlib, le_total, mulPosMono_iff_mulPosReflectLT, forall_lt_imp_le_iff_le_of_dense, ne_iff_lt_or_gt, Path.Homotopy.trans_apply, PUnit.not_lt, monotone_int_of_le_succ, instTrichotomousGt, forall_lt_iff_le, toPartialOrder_injective, ContinuousMap.Homotopy.trans_apply, not_lt_iff_eq_or_lt', addLeftStrictMono_of_addLeftReflectLE, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, LinearOrderedAddCommGroupWithTop.neg_top, CategoryTheory.TransfiniteCompositionOfShape.iic_F, LinearOrderedAddCommGroupWithTop.toIsOrderedAddMonoid, Ordering.compares_iff_of_compares_impl, exists_ge_of_linear, min_le_left, antitone_int_of_succ_le, instTrichotomousGe, forall_gt_iff_le, min_def, cmp_eq_eq_iff, NoBotOrder.to_noMinOrder, forall_gt_imp_ne_iff_le, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, le_or_gt, min_def_lt', max_def, le_imp_le_of_lt_imp_lt, not_lt, le_of_forall_lt_imp_ne, MulPosReflectLT.toMulPosMono, PosMulMono.toPosMulReflectLT, noBotOrder_iff_noMinOrder, strictAnti_int_of_succ_lt, posMulStrictMono_iff_posMulReflectLE, Path.trans_apply, Ne.gt_or_lt, instIsLinearOrder_mathlib, LinearOrderedCommMonoidWithZero.zero_le, ofDual_toAdd_eq_top_iff, addRightReflectLT_of_addRightMono, le_imp_le_iff_lt_imp_lt, top_add, Int.exists_strictMono, min_le_right, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, LinearOrderedAddCommMonoidWithTop.top_add', inv_lt_zero, cmp_eq_compareOfLessAndEq, compare_lt_iff_lt, dense_or_discrete', cmp_eq_gt_iff, cmp_eq_lt_iff, cmp_compares, Int.exists_strictAnti, PosMulStrictMono.toPosMulReflectLE, compare_of_injective_eq_compareOfLessAndEq, min_def_lt, ne_iff_gt_or_lt, covariant_lt_of_contravariant_le, AddValuation.mem_supp_iff, PUnit.instDenselyOrdered, gt_or_lt_of_ne, lt_or_ge, zpow_right_monoβ, NoTopOrder.to_noMaxOrder, compare_eq_compareOfLessAndEq, inv_nonpos, one_div_nonpos, exists_pair_lt, PosMulReflectLE.toPosMulStrictMono, bot_eq_zero'', zpow_right_strictMonoβ, le_total, lt_imp_lt_of_le_imp_le, LinearOrderedAddCommGroupWithTop.top_add', inv_lt_one_iffβ, le_of_forall_gt_imp_ne, compl_lt, PNat.coe_lt_coe, exists_le_of_linear, instIsStrictTotalOrderGt, lt_or_lt_iff_ne, nontrivial_iff_lt, not_monotone_not_antitone_iff_exists_lt_lt, le_max_left, min_def, forall_le_imp_ne_iff_lt, PNat.one_le, IsWellFounded.wellOrderExtension.isWellOrder_lt, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, ofAdd_toDual_eq_zero_iff, max_def, max_def_lt', compl_gt, LE.total', MulPosStrictMono.toMulPosReflectLE, lt_of_forall_ge_imp_ne, dense_or_discrete, compare_iff, Ne.lt_or_gt, LinearOrderedCommMonoidWithZero.toPosMulStrictMono, lt_trichotomy, compare_le_iff_le, instIsLinearOrderGe, MulPosMono.toMulPosReflectLT, MonomialOrder.lex_le_iff_of_unique, posMulMono_iff_posMulReflectLT, zpow_right_strictAntiβ, LE.total, mulLeftStrictMono_of_mulLeftReflectLE, instIsLinearOrderLe
|