| Name | Category | Theorems |
|---|
toDecidableEq π | CompOp | 170 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.ciSup_eq_max'_image, 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, Set.powersetCard.orderIsoOfFin_symm_apply_val, 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, 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'_image, 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, Ideal.IsHomogeneous.radical, 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, Ordinal.CNF.support_coeff, 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, Finset.ciInf_eq_min'_image, PMF.toOuterMeasure_bindOnSupport_apply, Profinite.NobelingProof.e_mem_of_eq_true, 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, ENat.epow_def, 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', Finset.min'_image, 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', Profinite.NobelingProof.eval_eq_ΟJ, compare_eq_compareOfLessAndEq, Profinite.NobelingProof.one_sub_e_mem_of_false, 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, Finset.Nonempty.ciSup_eq_max'_image, GenContFract.sub_convs_eq, Finset.insert_Icc_left_eq_Icc_pred, MultilinearMap.map_sub_map_piecewise, Ideal.IsHomogeneous.radical_eq, 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 | 49 mathmath: Finset.sorted_last_eq_max'_aux, List.sortedLE_mergeSort, ContDiffMapSupportedIn.iteratedFDerivLM_apply, ContDiffMapSupportedIn.structureMapCLM_apply, Finset.sortedGT_sort, ContDiffMapSupportedIn.monoLM_apply, Finset.orderIsoOfFin_symm_apply, Finset.sorted_zero_eq_min'_aux, Finset.sorted_last_eq_max', PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius, Set.powersetCard.orderIsoOfFin_apply_coe, Set.powersetCard.orderIsoOfFin_symm_apply_val, PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius, min_def', max_def', ContDiffMapSupportedIn.monoCLM_apply, List.sortedLE_insertionSort, Finset.sorted_zero_eq_min', 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, TestFunction.lineDerivCLM_apply, 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, 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, ContDiffMapSupportedIn.fderivLM_apply, TestFunction.monoCLM_apply, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, List.sortedGE_mergeSort, StrictMonoOn.map_finsetSort, oneLePart_eq_ite, min_def, List.sortedGE_insertionSort, Finset.listMap_orderEmbOfFin_finRange, max_def, ContDiffMapSupportedIn.structureMapLM_apply
|
toDecidableLT π | CompOp | 167 mathmath: Profinite.NobelingProof.GoodProducts.sum_to_range, sign_mul_self, Profinite.NobelingProof.injective_Οs', Finset.prod_one_sub_ordered, sign_eq_of_affineCombination_mem_affineSpan_pair, 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, EReal.sign_eq_and_abs_eq_iff_eq, sign_nonneg_iff, Profinite.NobelingProof.Products.eval_Οs, List.coe_maximum_of_length_pos, Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval, 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, EReal.abs_mul_sign, List.coe_le_maximum_iff, Profinite.NobelingProof.Οs'_apply_apply, sign_sum, 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, EReal.sign_mul, List.argmax_cons, Profinite.NobelingProof.GoodProducts.injective_sum_to, Order.PartialIso.exists_across, leOnePart_eq_ite_lt, EReal.sign_coe, 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, EReal.sign_bot, 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, Matrix.ProjGenLinGroup.val_signDet_mk, Profinite.NobelingProof.GoodProducts.square_commutes, min_def_lt', ENat.epow_def, MeasureTheory.stoppedProcess_eq_of_mem_finset, List.maximum_le_of_forall_le, Profinite.NobelingProof.contained_C1, Profinite.NobelingProof.isClosed_proj, EReal.sign_top, 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, EReal.le_iff_sign, 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.Products.isGood_mono, Profinite.NobelingProof.CC_comp_zero, EReal.sign_mul_inv_abs, min_def_lt, cmp_mul_neg_left, EReal.sign_mul_abs, 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, EReal.sign_neg, 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, EReal.sign_mul_inv_abs', 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 | 22 mathmath: le_max_right, eq_max, max_def_lt, max_left_comm, max_eq_right_of_lt, max_def', Max.left_comm, 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 | 291 mathmath: lt_or_gt_iff_ne', StrictMono.maximal_of_maximal_image, le_max_right, sq_lt_one_iffβ, not_le, ofDual_toAdd_zero, LinearOrderedAddCommGroupWithTop.neg_eq_top, LinearOrderedAddCommGroupWithTop.sub_pos, le_of_forall_lt_imp_le_of_dense, neg_of_div_neg_right, not_monotone_not_antitone_iff_exists_le_le, lt_or_gt_of_ne, Left.neg_of_mul_neg_left, lt_iff_not_ge, compl_le, toPartialOrder_injective_iff, instTrichotomousLt, IsWellFounded.wellOrderExtension.isWellFounded_lt, max_def_lt, zpow_right_antiβ, Eq.cmp_eq_eq', Ordering.Compares.cmp_eq, addLeftReflectLT_of_addLeftMono, LT.lt.gt_or_lt, AddValuation.top_iff, sq_lt_sqβ, addRightStrictMono_of_addRightReflectLE, Left.neg_of_mul_neg_right, isWellOrder_lt, zpow_left_injOnβ, Eq.cmp_eq_eq, LE.le.lt_or_ge, Function.Commute.iterate_pos_lt_iff_map_lt', LinearOrderedAddCommGroupWithTop.add_eq_top, neg_of_mul_neg_right, noTopOrder_iff_noMaxOrder, add_top, Ordinal.type_lt_ulift, MonotoneOn.reflect_lt, PUnit.le, inv_le_one_iffβ, lt_of_pow_lt_pow_leftβ, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, Function.Commute.iterate_pos_lt_iff_map_lt, isWellOrder_gt, one_lt_sq_iffβ, gt_trichotomy, Right.neg_of_mul_neg_right, instTrichotomousLe, Right.neg_of_mul_neg_left, neg_of_mul_neg_left, Monotone.strictMono_iff_injective, CategoryTheory.TransfiniteCompositionOfShape.ici_F, ContinuousMap.HomotopyRel.trans_apply, one_div_neg, lt_of_not_ge, Antitone.reflect_lt, compare_gt_iff_gt, instIsStrictTotalOrderLt, le_iff_le_iff_lt_iff_lt, MulPosReflectLE.toMulPosStrictMono, StrictAnti.cmp_map_eq, PNat.not_lt_one, StrictAnti.compares, cmp_self_eq_eq, cmp_eq_cmp_symm, Antitone.strictAnti_iff_injective, StrictMono.lt_iff_lt, pos_and_pos_or_neg_and_neg_of_mul_pos, lt_iff_lt_of_cmp_eq_cmp, ofAdd_bot, Path.Homotopy.hcomp_apply, LinearOrderedAddCommGroupWithTop.sub_top, covariant_le_iff_contravariant_lt, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, MonomialOrder.lex_lt_iff_of_unique, StrictAntiOn.cmp_map_eq, LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid, LE.le.ge_or_le, zpow_le_zpow_iff_leftβ, sq_le_one_iffβ, one_lt_pow_iff_of_nonneg, LT.lt.cmp_eq_gt, le_of_not_gt, not_lt_iff_eq_or_lt, covariant_lt_iff_contravariant_le, mulPosStrictMono_iff_mulPosReflectLE, ArchimedeanClass.FiniteElement.mk_add_mk, PNat.coe_le_coe, mulRightReflectLT_of_mulRightMono, LinearOrderedAddCommGroupWithTop.neg_pos, AntitoneOn.reflect_lt, neg_of_mul_pos_right, min_def', pow_le_pow_iff_leftβ, Monotone.reflect_lt, strictMono_int_of_lt_succ, lt_min, max_def', LinearOrderedAddCommGroupWithTop.top_pos, pow_lt_one_iff_of_nonneg, PosMulReflectLT.toPosMulMono, forall_ge_imp_ne_iff_lt, forall_gt_imp_ge_iff_le_of_dense, le_iff_le_of_cmp_eq_cmp, mulRightStrictMono_of_mulRightReflectLE, StrictAntiOn.le_iff_ge, IicProdIoc_def, le_of_not_ge, 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, LT.lt.cmp_eq_lt, mulLeftReflectLT_of_mulLeftMono, instLawfulBCmpCompare_mathlib, le_total, StrictMono.minimal_preimage_bot, mulPosMono_iff_mulPosReflectLT, forall_lt_imp_le_iff_le_of_dense, div_nonpos_of_nonneg_of_nonpos, ne_iff_lt_or_gt, StrictMono.minimal_of_minimal_image, Path.Homotopy.trans_apply, PUnit.not_lt, monotone_int_of_le_succ, instTrichotomousGt, sq_le_sqβ, forall_lt_iff_le, toPartialOrder_injective, neg_iff_neg_of_mul_pos, ContinuousMap.Homotopy.trans_apply, not_lt_iff_eq_or_lt', addLeftStrictMono_of_addLeftReflectLE, max_lt, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, LinearOrderedAddCommGroupWithTop.neg_top, Function.Commute.iterate_pos_le_iff_map_le', CategoryTheory.TransfiniteCompositionOfShape.iic_F, le_min, LT.lt.lt_or_gt, LinearOrderedAddCommGroupWithTop.toIsOrderedAddMonoid, Ordering.compares_iff_of_compares_impl, exists_ge_of_linear, min_le_left, antitone_int_of_succ_le, le_of_forall_lt, StrictAntiOn.lt_iff_gt, instTrichotomousGe, StrictMonoOn.cmp_map_eq, one_le_pow_iff_of_nonneg, forall_gt_iff_le, min_def, cmp_eq_eq_iff, one_le_sq_iffβ, NoBotOrder.to_noMinOrder, forall_gt_imp_ne_iff_le, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, le_or_gt, min_def_lt', max_def, StrictMono.maximal_preimage_top, zpow_lt_zpow_iff_leftβ, le_imp_le_of_lt_imp_lt, LE.le.le_or_gt, LE.le.gt_or_le, pow_le_one_iff_of_nonneg, not_lt, StrictAnti.le_iff_ge, le_of_forall_lt_imp_ne, Ordinal.ord_cof_eq, MulPosReflectLT.toMulPosMono, lt_of_mul_self_lt_mul_selfβ, PosMulMono.toPosMulReflectLT, noBotOrder_iff_noMinOrder, MonotoneOn.strictMonoOn_iff_injOn, strictAnti_int_of_succ_lt, StrictAnti.minimal_of_maximal_image, posMulStrictMono_iff_posMulReflectLE, Path.trans_apply, Ne.gt_or_lt, instIsLinearOrder_mathlib, LinearOrderedCommMonoidWithZero.zero_le, ofDual_toAdd_eq_top_iff, addRightReflectLT_of_addRightMono, StrictMono.cmp_map_eq, le_imp_le_iff_lt_imp_lt, max_le, top_add, Int.exists_strictMono, min_le_right, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, LinearOrderedAddCommMonoidWithTop.top_add', inv_lt_zero, cmp_eq_compareOfLessAndEq, StrictAntiOn.compares, compare_lt_iff_lt, dense_or_discrete', Function.Commute.iterate_pos_le_iff_map_le, LE.le.le_or_ge, cmp_eq_gt_iff, cmp_eq_lt_iff, AntitoneOn.strictAnti_iff_injOn, cmp_compares, Int.exists_strictAnti, PosMulStrictMono.toPosMulReflectLE, le_of_forall_gt_imp_ge_of_dense, Ordinal.typein_lt_nat, compare_of_injective_eq_compareOfLessAndEq, min_def_lt, ne_iff_gt_or_lt, covariant_lt_of_contravariant_le, AddValuation.mem_supp_iff, PUnit.instDenselyOrdered, LE.le.ge_or_lt, eq_or_gt_of_not_lt, gt_or_lt_of_ne, lt_or_ge, zpow_right_monoβ, le_of_pow_le_pow_leftβ, NoTopOrder.to_noMaxOrder, compare_eq_compareOfLessAndEq, StrictMonoOn.le_iff_le, inv_nonpos, one_div_nonpos, exists_pair_lt, Ordinal.type_Iio_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, StrictAnti.lt_iff_gt, StrictMono.le_iff_le, exists_le_of_linear, instIsStrictTotalOrderGt, StrictAnti.maximal_of_minimal_image, eq_or_lt_of_not_gt, lt_or_lt_iff_ne, nontrivial_iff_lt, neg_of_mul_pos_left, not_monotone_not_antitone_iff_exists_lt_lt, le_max_left, min_def, forall_le_imp_ne_iff_lt, PNat.one_le, lt_iff_lt_of_le_iff_le, IsWellFounded.wellOrderExtension.isWellOrder_lt, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, ofAdd_toDual_eq_zero_iff, max_def, StrictMonoOn.compares, max_def_lt', compl_gt, le_of_forall_gt, LE.total', MulPosStrictMono.toMulPosReflectLE, lt_of_forall_ge_imp_ne, dense_or_discrete, StrictMono.compares, compare_iff, Ne.lt_or_gt, neg_of_div_neg_left, LinearOrderedCommMonoidWithZero.toPosMulStrictMono, pow_lt_pow_iff_leftβ, lt_trichotomy, compare_le_iff_le, instIsLinearOrderGe, StrictMonoOn.lt_iff_lt, MulPosMono.toMulPosReflectLT, MonomialOrder.lex_le_iff_of_unique, posMulMono_iff_posMulReflectLT, zpow_right_strictAntiβ, List.IsChain.cons_of_le, LE.total, mulLeftStrictMono_of_mulLeftReflectLE, GaloisConnection.lt_iff_lt, ArchimedeanClass.FiniteElement.mk_sub_mk, instIsLinearOrderLe
|