| Name | Category | Theorems |
|---|
Antitone 📖 | MathDef | 221 mathmath: seminormFromConst_seq_antitone, fixingSubgroup_antitone, Dynamics.coverEntropyInfEntourage_antitone, Antitone.iInf, Antitone.union, not_monotone_not_antitone_iff_exists_le_le, Monotone.mul_const_of_nonpos, Antitone.sInf, MeasureTheory.GridLines.T_lmarginal_antitone, Antitone.mul_const', zpow_right_anti₀, antitone_continuousOn, ArchimedeanClass.addSubgroup_antitone, lowerPolar_anti, antitone_mul_left, Monotone.Ici, Subsingleton.antitone', LinearMap.polar_antitone, lowerCentralSeries_antitone, Monotone.Ioo, t2Space_antitone, negPart_anti, Finset.antitone_iff_forall_insert_le, inv_pow_anti, Function.antitone_iterate_of_le_id, StrictAnti.trans_monovary, Antivary.exists_antitone_monotone, LinearMap.singularValues_antitone, Antitone.sSup, antitone_Ioi, Set.antitoneOn_iff_antitone, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map, Dynamics.netEntropyEntourage_antitone, Antitone.exists, compl_anti, antitone_le, Antitone.mul', Set.antitone_setOf, derivedSeries_antitone, Antitone.add_const, Antitone.comp_monotone, MeasureTheory.hittingBtwn_apply_anti, Antitone.const_add, antitone_add_nat_iff_antitoneOn_nat_Ici, Stirling.stirlingSeq'_antitone, antitone_toDual_comp_iff, StrictMono.trans_antivary, antitone_iff_map_nonpos, IntermediateField.fixedField_antitone, Antitone.apply₂, PointedCone.dual_antitone, Monotone.Ico, Antitone.set_prod, Dynamics.coverMincard_antitone, monotone_toDual_comp_iff, Dynamics.netMaxcard_antitone, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, Antitone.Iio, Order.PFilter.antitone_principal, Finsupp.DegLex.single_antitone, Finset.prod_anti_set_of_le_one', t1Space_antitone, Antitone.mul_monotone, Matrix.IsHermitian.eigenvalues₀_antitone, antitone_of_odd_of_monotoneOn_nonneg, Monotone.dual_left, Real.antitone_arccos, antitone_lam, antitone_iff_map_nonneg, antitone_iff_forall_wcovBy, Dynamics.coverEntropy_antitone, antitone_prod_iff, antivary_iff_exists_monotone_antitone, preCantorSet_antitone, LieModule.antitone_lowerCentralSeries, MeasureTheory.hittingBtwn_anti, Filter.exists_seq_antitone_tendsto_atTop_atBot, monovary_iff_exists_antitone, Filter.antitone_seq_of_seq, OrdinalApprox.gfpApprox_antitone, fixingSubmonoid_antitone, antitone_vecCons, Real.antitone_rpow_of_base_le_one, fixedPoints_addSubgroup_antitone, AddConstMapClass.antitone_iff_Icc, MeasureTheory.hittingAfter_apply_anti, Antitone.dual, MulArchimedeanClass.ballSubgroup_antitone, IntermediateField.fixingSubgroup_antitone, Finset.sum_anti_set_of_nonpos', Set.monotone_or_antitone_iff_uIcc, AntitoneOn.Iic_union_Ici, Ideal.Filtration.antitone, CategoryTheory.MorphismProperty.antitone_rlp, antitone_of_le_pred, Pi.zero_anti, AntitoneOn.exists_antitone_extension, Antitone.inf, antitone_dual_iff, Set.antitone_bforall, ArchimedeanClass.ballAddSubgroup_antitone, antitone_of_deriv_nonpos, Dynamics.coverEntropyInf_antitone, antitone_smul_left, Monotone.dual_right, Antitone.partMap, antitone_int_of_succ_le, List.SortedGE.antitone, Monotone.Ioc, Monotone.inv, AffineMap.lineMap_anti, antitone_add_nat_of_succ_le, isLowerSet_setOf, Antitone.partSeq, NNReal.agmSequences_monotone_and_antitone, Monotone.neg, Stirling.log_stirlingSeq'_antitone, CategoryTheory.Triangulated.TStructure.ge_antitone, Antitone.leftLim, MeasureTheory.Egorov.notConvergentSeq_antitone, antitone_nat_of_succ_le, antitone_iff_apply₂, antitone_mul_right, Monotone.mul_antitone, Dynamics.coverEntropyEntourage_antitone, Monotone.Ioi, pow_right_anti₀, antivary_id_iff, Set.antitone_mem, Monotone.const_mul_of_nonpos, CStarAlgebra.pow_antitone, antitoneOn_univ, compl_antitone, antitone_iff_forall_covBy, antitone_of_hasDerivAt_nonpos, Finsupp.Lex.single_antitone, Set.antitone_dissipate, Pi.one_anti, Antitone.iSup, fixedPoints_subgroup_antitone, fixingAddSubmonoid_antitone, antitone_app, Antitone.rightLim, fixedPoints_antitone_addSubmonoid, Antitone.inter, CategoryTheory.MorphismProperty.antitone_llp, SimpleGraph.egirth_anti, PairReduction.antitone_logSizeBallSeq_add_one_subset, MulArchimedeanClass.subgroup_antitone, List.sorted_ge_ofFn_iff, Antitone.forall, Equiv.image_antitone, fixingAddSubgroup_antitone, Monotone.antitone_iterate_of_map_le, antitone_Ici, Fin.antitone_iff_succ_le, antitone_of_le_sub_one, IsGLB.exists_seq_antitone_tendsto, antitone_lt, Antitone.Iic, Antitone.mul_const, Filter.IsAntitoneBasis.antitone, List.sortedGE_iff_antitone_get, NNReal.agmSequences_snd_antitone, Antitone.ball, List.SortedGE.antitone_get, Antitone.prodMap, Subsingleton.antitone, antitone_iff_forall_lt, isClosed_antitone, antitone_const, Filter.HasAntitoneBasis.antitone, antitone_comp_ofDual_iff, Order.coheight_anti, Monotone.Icc, exists_seq_tendsto_sInf, Antitone.vecCons, one_div_pow_anti, Antitone.covariant_of_const', Directed.sequence_anti, borel_anti, AntitoneOn.monotone, Filter.exists_antitone_seq, MvPolynomial.IsSymmetric.antitone_supDegree, monotone_comp_ofDual_iff, antitone_of_add_one_le, Dynamics.netEntropyInfEntourage_antitone, Fin.rev_anti, hnot_anti, upperPolar_anti, antitone_const_tsub, Dynamics.dynEntourage_antitone, Antitone.max, not_monotone_not_antitone_iff_exists_lt_lt, antitone_of_succ_le, fixedPoints_antitone, Monotone.comp_antitone, Finset.prod_anti_set_of_le_one, Antitone.const_mul, antitone_vecEmpty, MeasureTheory.hittingAfter_anti, Antivary.exists_monotone_antitone, Antitone.of_apply₂, ArchimedeanClass.ball_antitone, Antitone.partBind, List.sortedGE_ofFn_iff, integral_sin_pow_antitone, Finset.antitone_iff_forall_cons_le, EReal.antitone_div_right_of_nonpos, Antitone.const_mul', Antitone.covariant_of_const, Antitone.sup, antivary_iff_exists_antitone_monotone, LinearMap.IsSymmetric.eigenvalues_antitone, Antitone.add, Monovary.exists_antitone, StrictAnti.antitone, BoxIntegral.Box.antitone_lower, upperClosure_anti, Antitone.min, leOnePart_anti
|
AntitoneOn 📖 | MathDef | 103 mathmath: Set.Subsingleton.antitoneOn, MonotoneOn.dual_left, MonotoneOn.Icc, AntitoneOn.set_prod, antitoneOn_of_hasDerivWithinAt_nonpos, sub_inv_antitoneOn_Ioi, variationOnFromTo.antitoneOn, SimpleGraph.antitoneOn_extremalNumber_div_choose_two, Antitone.antitoneOn, monotoneOn_comp_ofDual_iff, MonotoneOn.neg, quasilinearOn_iff_monotoneOn_or_antitoneOn, antitoneOn_const, AntitoneOn.const_add, Real.antitoneOn_cos, Set.antitoneOn_iff_antitone, AntivaryOn.exists_antitoneOn_monotoneOn, ConcaveOn.antitoneOn_slope_gt, Set.EqOn.congr_antitoneOn, AntitoneOn.mul', AntitoneOn.inter, Nat.clog_antitone_left, antitone_add_nat_iff_antitoneOn_nat_Ici, MonotoneOn.Ici, AntitoneOn.mul_const', AntitoneOn.union, sub_inv_antitoneOn_Icc_left, AntitoneOn.of_map_sup, antitoneOn_of_le_pred, ConcaveOn.slope_anti, antitoneOn_toDual_comp_iff, Set.monotoneOn_or_antitoneOn_iff_uIcc, isClosed_antitoneOn, ConcaveOn.antitoneOn_slope_lt, Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le, antitoneOn_of_le_sub_one, AntitoneOn.min, antivaryOn_iff_exists_monotoneOn_antitoneOn, Nat.log_antitone_left, MulArchimedeanClass.mk_antitoneOn, AddConstMapClass.antitone_iff_Icc, AntitoneOn.mono, Real.log_div_self_antitoneOn, AntitoneOn.Iic, antitoneOn_nat_Ici_of_succ_le, antitoneOn_comp_ofDual_iff, Real.log_div_sqrt_antitoneOn, AntitoneOn.max, AntitoneOn.const_mul', antitoneOn_of_succ_le, antitoneOn_inv_pos, inv_antitoneOn_Icc_right, AntitoneOn.union_right, AntitoneOn.inf, MonotoneOn.inv, AntitoneOn.sup, monotoneOn_toDual_comp_iff, AntitoneOn.Iio, antitoneOn_univ, AntitoneOn.of_map_inf, QuasilinearOn.monotoneOn_or_antitoneOn, antitoneOn_dual_iff, AntitoneOn.add_const, MonotoneOn.comp_AntitoneOn, MonotoneOn.Ico, antitoneOn_of_add_one_le, dist_anti_right_pi, MeasureTheory.integral_antitoneOn_of_integrand_ae, AntivaryOn.exists_monotoneOn_antitoneOn, antivaryOn_id_iff, MonotoneOn.Ioc, MonotoneOn.dual_right, AntitoneOn.congr, Antitone.comp_monotoneOn, StrictAntiOn.antitoneOn, ConcaveOn.antitoneOn_derivWithin, Set.antitoneOn_insert_iff, sub_inv_antitoneOn_Icc_right, MonotoneOn.Ioo, inv_antitoneOn_Ioi, MonovaryOn.exists_antitoneOn, Real.antitoneOn_rpow_Ioi_of_exponent_nonpos, StrictMonoOn.trans_antivaryOn, antivaryOn_iff_exists_antitoneOn_monotoneOn, AntitoneOn.add, Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt, antitoneOn_of_deriv_nonpos, Monotone.comp_antitoneOn, Set.antitoneOn_singleton, monovaryOn_iff_exists_antitoneOn, ArchimedeanClass.mk_antitoneOn, MonotoneOn.Ioi, StrictAntiOn.trans_monovaryOn, Real.log_div_self_rpow_antitoneOn, antitoneOn_iff_forall_lt, ConcaveOn.antitoneOn_deriv, sub_inv_antitoneOn_Iio, Function.antitoneOn_of_rightInvOn_of_mapsTo, inv_antitoneOn_Icc_left, AntitoneOn.comp_MonotoneOn, inv_antitoneOn_Iio, dist_anti_left_pi, AntitoneOn.dual
|
MonotoneOn 📖 | MathDef | 111 mathmath: Antitone.comp_antitoneOn, MonotoneOn.insert_of_continuousWithinAt, CFC.monotoneOn_one_sub_one_add_inv, MonotoneOn.of_map_inf, ConvexOn.monotoneOn_slope_lt, Real.rpowIntegrand₀₁_monotoneOn, monotoneOn_iff_forall_lt, AntitoneOn.Ici, monotoneOn_of_sub_one_le, MonotoneOn.max, MonotoneOn.union, AntitoneOn.neg, MonotoneOn.inf, Real.log_mul_self_monotoneOn, MonovaryOn.exists_monotoneOn, monotoneOn_comp_ofDual_iff, ConvexOn.monotoneOn_rightDeriv, quasilinearOn_iff_monotoneOn_or_antitoneOn, Real.monotoneOn_posLog, AntitoneOn.Icc, monotone_add_nat_iff_monotoneOn_nat_Ici, MonotoneOn.of_map_sup, monotoneOn_descPochhammer_eval, MonotoneOn.Iio, AntivaryOn.exists_antitoneOn_monotoneOn, StrictAntiOn.trans_antivaryOn, MonotoneOn.const_add, Cardinal.toNat_monotoneOn, ArchimedeanClass.mk_monotoneOn, MonotoneOn.congr, MonotoneOn.const_mul', antitoneOn_toDual_comp_iff, Set.monotoneOn_iff_monotone, Set.monotoneOn_or_antitoneOn_iff_uIcc, monotoneOn_of_le_add_one, monotoneOn_deriv_descPochhammer_eval, Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le, Real.monotoneOn_rpow_Ici_of_exponent_nonneg, monotoneOn_of_hasDerivWithinAt_nonneg, monotoneOn_of_deriv_nonneg, monovaryOn_iff_exists_monotoneOn, monotoneOn_nat_Ici_of_le_succ, AntitoneOn.dual_right, antivaryOn_iff_exists_monotoneOn_antitoneOn, MonotoneOn.Iic, monotoneOn_const, ConvexOn.monotoneOn_deriv, MonotoneOn.add, MulArchimedeanClass.mk_monotoneOn, CFC.log_monotoneOn, MonotoneOn.sup, CFC.monotoneOn_one_sub_one_add_inv_real, AntitoneOn.Ioi, pow_left_monotoneOn, MonotoneOn.add_const, dist_mono_left_pi, MonotoneOn.inter, StrictMonoOn.trans_monovaryOn, ConvexOn.slope_mono, ArchimedeanClass.stdPart_monotoneOn, AddConstMapClass.monotone_iff_Icc, antitoneOn_comp_ofDual_iff, AntitoneOn.dual_left, MonotoneOn.mul, monotoneOn_of_le_succ, ConvexOn.monotoneOn_leftDeriv, variationOnFromTo.sub_self_monotoneOn, AntitoneOn.inv, MonotoneOn.dual, AntitoneOn.Ioo, AntitoneOn.comp, Nat.pow_monotoneOn, Set.Subsingleton.monotoneOn, Set.monotoneOn_singleton, MonotoneOn.mul', monotoneOn_toDual_comp_iff, monotoneOn_id, LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn, StrictMonoOn.monotoneOn, QuasilinearOn.monotoneOn_or_antitoneOn, MonotoneOn.comp, monotoneOn_of_pred_le, variationOnFromTo.monotoneOn, Function.locallyFinsuppWithin.logCounting_mono, Function.monotoneOn_of_rightInvOn_of_mapsTo, monovaryOn_id_iff, AntivaryOn.exists_monotoneOn_antitoneOn, Real.monotoneOn_sin, ConvexOn.monotoneOn_derivWithin, ConvexOn.monotoneOn_slope_gt, MonotoneOn.set_prod, antivaryOn_iff_exists_antitoneOn_monotoneOn, dist_mono_right_pi, Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt, Set.monotoneOn_insert_iff, Monotone.monotoneOn, AntitoneOn.Ioc, AntitoneOn.Ico, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, MeasureTheory.integral_monotoneOn_of_integrand_ae, monotoneOn_dual_iff, zpow_left_monoOn₀, Set.EqOn.congr_monotoneOn, isClosed_monotoneOn, ValueDistribution.logCounting_monotoneOn, MonotoneOn.mul_const', monotoneOn_univ, MonotoneOn.union_right, Monotone.comp_monotoneOn, MonotoneOn.mono, MonotoneOn.min
|
StrictAnti 📖 | MathDef | 117 mathmath: zpow_right_strictAnti, Continuous.strictMono_of_inj_boundedOrder', StrictMono.strictAnti_iterate_of_map_lt, Nat.exists_strictAnti', unitInterval.strictAnti_symm, StrictAnti.mul_antitone', one_div_pow_strictAnti, exists_seq_strictAnti_tendsto', strictAnti_vecEmpty, StrictMono.neg, EReal.neg_strictAnti, exists_seq_strictAnti_tendsto, strictAnti_mul_right, StrictAnti.comp_strictMono, CategoryTheory.isArtinianObject_iff_not_strictAnti, Finsupp.Lex.single_strictAnti, inv_pow_strictAnti, Antitone.mul_strictAnti', List.SortedGT.strictAnti, StrictAnti.mul', StrictMono.dual_right, StrictMono.const_mul_of_neg, MulArchimedeanClass.subsemigroup_strictAnti, StrictAnti.const_mul, WellFoundedGT.rank_strictAnti, StrictMono.inv, Antitone.strictAnti_iff_injective, strictAnti_smul_left, Dense.exists_seq_strictAnti_tendsto_of_lt, WithBot.strictAnti_iff, EReal.strictAnti_div_right_of_neg, IsGLB.exists_seq_strictAnti_tendsto_of_notMem, StrictAnti.prodMap, Antitone.add_strictAnti, strictMono_comp_ofDual_iff, Real.exists_seq_rat_strictAnti_tendsto, exists_seq_strictAnti_strictMono_tendsto, Real.strictAnti_eulerMascheroniSeq', strictAnti_toDual_comp_iff, List.SortedGT.strictAnti_get, List.sortedGT_iff_strictAnti_get, List.sorted_gt_ofFn_iff, AkraBazziRecurrence.strictAnti_sumCoeffsExp, ENNReal.inv_strictAnti, StrictAnti.mul_const', Subsingleton.strictAnti, strictAnti_iff_map_neg, strictAnti_of_odd_strictAntiOn_nonneg, strictAnti_of_succ_lt, StrictMono.dual_left, strictAnti_of_lt_sub_one, strictAnti_mul_left, ArchimedeanClass.subsemigroup_strictAnti, Equiv.image_strictAnti, strictAnti_iff_map_pos, zsmul_left_strictAnti, StrictAnti.const_mul', AddConstMapClass.strictAnti_iff_Icc, pow_right_strictAnti₀, List.sortedGT_ofFn_iff, StrictAnti.vecCons, WithTop.strictAnti_iff, strictAnti_of_deriv_neg, StrictAnti.add, StrictAnti.add_const, strictAnti_dual_iff, Continuous.strictMono_of_inj, StrictAnti.dual, StrictAnti.add_antitone, compl_strictAnti, Concept.strictAnti_intent, strictAnti_int_of_succ_lt, StrictMono.mul_const_of_neg, StrictMono.comp_strictAnti, Antitone.strictAnti_of_injective, Dense.exists_seq_strictAnti_tendsto, FiniteArchimedeanClass.addSubgroup_strictAnti, strictAnti_of_le_iff_le, StrictAntiOn.Iic_union_Ici, FiniteMulArchimedeanClass.ballSubgroup_strictAnti, Real.strictAnti_rpow_of_base_lt_one, StrictAntiOn.strictAnti, strictAnti_nat_of_succ_lt, Ideal.pow_right_strictAnti, Continuous.strictAnti_of_inj_boundedOrder, Int.exists_strictAnti, strictAnti_iff_forall_covBy, FiniteArchimedeanClass.ballAddSubgroup_strictAnti, FiniteArchimedeanClass.submodule_strictAnti, strictAntiOn_univ, strictAnti_of_add_one_lt, exists_seq_strictAnti_tendsto_nhdsWithin, Fin.rev_strictAnti, FiniteArchimedeanClass.ball_strictAnti, Finset.strictAnti_iff_forall_cons_lt, strictAnti_of_hasDerivAt_neg, Set.range_injOn_strictAnti, Fin.strictAnti_iff_succ_lt, strictAnti_vecCons, StrictAnti.ite, mulintEquivOfZPowersEqTop_strictAnti, FiniteMulArchimedeanClass.subgroup_strictAnti, StrictAnti.mul_const, DenseRange.exists_seq_strictAnti_tendsto_of_lt, strictMono_toDual_comp_iff, Set.strictAntiOn_iff_strictAnti, StrictAnti.const_add, strictAnti_of_lt_pred, Nat.exists_strictAnti, StrictAnti.ite', Finset.strictAnti_iff_forall_lt_insert, strictAnti_comp_ofDual_iff, Finsupp.DegLex.single_strictAnti, DenseRange.exists_seq_strictAnti_tendsto, zpow_right_strictAnti₀, CategoryTheory.not_strictAnti_of_isArtinianObject, not_strictAnti_of_wellFoundedLT
|
StrictAntiOn 📖 | MathDef | 73 mathmath: EReal.inv_strictAntiOn, Set.Subsingleton.strictAntiOn, strictAntiOn_toDual_comp_iff, MulArchimedeanClass.subgroup_strictAntiOn, strictAntiOn_of_lt_sub_one, Real.strictAntiOn_logb, Int.strictAntiOn_natAbs, strictAntiOn_comp_ofDual_iff, Real.strictAntiOn_arccos, StrictAntiOn.dual, Real.Gamma_strictAntiOn_Ioc, StrictMono.comp_strictAntiOn, inv_strictAntiOn, StrictAntiOn.add, one_div_strictAntiOn, StrictMonoOn.dual_left, StrictMonoOn.comp_strictAntiOn, StrictAntiOn.comp_strictMonoOn, StrictMonoOn.neg, ContinuousOn.strictMonoOn_of_injOn_Icc', StrictAntiOn.const_mul', Set.EqOn.congr_strictAntiOn, StrictAntiOn.const_add, Polynomial.Chebyshev.strictAntiOn_node, StrictAntiOn.congr, ContinuousOn.strictMonoOn_of_injOn_Ioo, Real.strictAntiOn_rpow_Ioi_of_exponent_neg, Set.strictAntiOn_singleton, strictAntiOn_insert_iff, StrictAnti.comp_strictMonoOn, AkraBazziRecurrence.strictAntiOn_one_add_smoothingFn, Real.qaryEntropy_strictAntiOn, strictMonoOn_toDual_comp_iff, StrictConcaveOn.strictAntiOn_deriv, StrictAntiOn.mul', strictAntiOn_of_succ_lt, AddConstMapClass.strictAnti_iff_Icc, ConvexOn.strictAntiOn, Real.strictAntiOn_logb_of_base_lt_one, StrictAntiOn.add_const, StrictConcaveOn.strictAntiOn_derivWithin, StrictMonoOn.inv, StrictAnti.strictAntiOn, strictAntiOn_of_lt_pred, strictAntiOn_insert_iff_of_forall_ge, AntitoneOn.strictAnti_iff_injOn, strictAntiOn_of_deriv_neg, Real.strictAntiOn_log, ArchimedeanClass.addSubgroup_strictAntiOn, StrictAntiOn.union, strictAntiOn_univ, strictAntiOn_Iic_of_succ_lt, strictAntiOn_of_hasDerivWithinAt_neg, Real.strictAntiOn_cos, strictAntiOn_Ici_of_lt_pred, StrictAntiOn.mono, Real.binEntropy_strictAntiOn, StrictAntiOn.mul_antitone', AntitoneOn.strictAntiOn_of_injOn, strictAntiOn_inv_pos, AntitoneOn.add_strictAnti, strictAntiOn_insert_iff_of_forall_le, ConcaveOn.strictAntiOn, StrictMonoOn.dual_right, strictMonoOn_comp_ofDual_iff, AntitoneOn.mul_strictAnti', Set.strictAntiOn_iff_strictAnti, strictAntiOn_dual_iff, StrictAntiOn.mul_const', strictAntiOn_of_add_one_lt, ContinuousOn.strictAntiOn_of_injOn_Icc, StrictAntiOn.add_antitone, AkraBazziRecurrence.strictAntiOn_smoothingFn
|
StrictMono 📖 | MathDef | 434 mathmath: Finset.val_strictMono, MulEquiv.strictMono_symm, Ordinal.isNormal_iff_strictMono_limit, add_right_strictMono, GaloisInsertion.strictMono_u, Continuous.strictMono_of_inj_boundedOrder', ENNReal.pow_right_strictMono, SSet.stdSimplex.mem_nonDegenerate_iff_strictMono, NNRat.cast_strictMono, Fin.strictMono_pred_comp, WithBotTop.coe_strictMono, StrictMono.const_add, Nat.exists_strictMono, Polynomial.Sequence.basis_natDegree_strictMono, Finset.card_strictMono, StrictMono.mul, Finsupp.toMultiset_strictMono, strictMono_of_hasDerivAt_pos, Filter.extraction_forall_of_frequently, IsFractionRing.coeSubmodule_strictMono, AddSubmonoid.comap_strictMono_of_surjective, Nat.exists_strictMono', StrictMono.const_mul, add_right_strictMono_of_ne_top, ack_strictMono_left, strictMono_nhdsSet, add_left_strictMono, EReal.exp_strictMono, NonUnitalSubring.toNonUnitalSubsemiring_strictMono, Function.update_strictMono, OrderAddMonoidIso.strictMono_symm, strictMono_of_lt_add_one, AddMonoidHom.inl_strictMono, exists_seq_strictMono_tendsto_nhdsWithin, strictMono_dual_iff, grade_strictMono, FirstOrder.Language.Substructure.comap_strictMono_of_surjective, ENat.toENNReal_strictMono, RingPreordering.toSubsemiring_strictMono, MonoidWithZeroHom.ValueGroup₀.monoidWithZeroHom_strictMono, RingCon.matrix_strictMono_of_nonempty, Ordinal.deriv_strictMono, LowerSet.Iio_strictMono, Subgroup.ofUnits_strictMono, WithTop.pow_right_strictMono, Fin.strictMono_succAbove, OrderIso.strictMono, WithZero.map'_strictMono, strictMono_of_lt_succ, Nat.nth_strictMono, unitInterval.sigmoid_strictMono, NonemptyInterval.toLex_strictMono, Submonoid.comap_strictMono_of_surjective, EReal.strictMono_div_right_of_pos, Sum.Lex.inr_strictMono, NonUnitalSubsemiring.toAddSubmonoid_strictMono, mul_right_strictMono, strictMono_nat_of_lt_succ, StrictMono.add_monotone, HahnEmbedding.Seed.baseEmbedding_strictMono, RingHom.strictMono_comap_of_surjective, CircleDeg1Lift.strictMono_iff_injective, Finset.Colex.toColex_strictMono, ValuativeRel.ValueGroupWithZero.embed_strictMono, Filter.extraction_of_eventually_atTop, MonomialOrder.toSyn_strictMono, SeqCompactSpace.tendsto_subseq, Multiset.disjSum_strictMono_left, Monotone.strictMono_iff_injective, ENat.map_natCast_strictMono, algebraMap_strictMono, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, ENNReal.log_strictMono, HahnEmbedding.Seed.strictMono_coeff, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, DenseRange.exists_seq_strictMono_tendsto, StrictMono.mul', Ordinal.veblenWith_right_strictMono, TopologicalSpace.IrreducibleCloseds.map_strictMono_of_isInducing, Pell.strictMono_y, strictMono_of_odd_strictMonoOn_nonneg, strictMono_vecEmpty, Filter.extraction_forall_of_eventually, Ordinal.veblenWith_zero_strictMono, StrictMono.ite, Monotone.mul_strictMono, Set.ecard_strictMono, zpow_right_strictMono, WithTop.strictMono_map_iff, Finset.disjSum_strictMono_left, HahnEmbedding.Partial.extendFun_strictMono, Cardinal.mul_natCast_strictMono, strictMono_of_sub_one_lt, add_left_strictMono_of_ne_top, ValuativeExtension.mapValueGroupWithZero_strictMono, StrictMono.const_nsmul, Set.encard_strictMono, Submodule.height_strictMono, CategoryTheory.not_strictMono_of_isNoetherianObject, Submodule.strictMono_comap_prod_map, Function.const_strictMono, IsSeqCompact.subseq_of_frequently_in, MonoidWithZeroHom.inl_strictMono, not_strictMono_of_wellFoundedGT, DenseRange.exists_seq_strictMono_tendsto_of_lt, Polynomial.Sequence.natDegree_strictMono, IsCompact.tendsto_subseq', Real.sinh_sub_id_strictMono, Fin.strictMono_castPred_comp, Int.cast_strictMono, Submodule.toAddSubmonoid_strictMono, Subgroup.toSubmonoid_strictMono, Ordinal.toZFSet_strictMono, strictMono_of_deriv_pos, HahnEmbedding.IsPartial.strictMono, strictMono_mersenne, strictMono_iff_map_pos, Order.succ_strictMono, MulEquiv.strictMono_subsemigroupCongr, MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq_strictMono, FractionalIdeal.mul_left_strictMono, List.foldr_strictMono, StrictMono.withBot_map, Finset.geomSum_ofColex_strictMono, strictMono_comp_ofDual_iff, Real.strictMono_eulerMascheroniSeq, StrictMono.div_const, OrderEmbedding.strictMono, Filter.subseq_tendsto_of_neBot, LocallyFiniteOrder.orderAddMonoidHom_strictMono, QuotientAddGroup.strictMono_comap_prod_image, StrictMono.vecCons, NonUnitalSubsemiring.toSubsemigroup_strictMono, WithZero.withZeroUnitsEquiv_symm_strictMono, WithVal.strictMono_valueGroupOrderIso₀, Polynomial.card_support_eq, Filter.Tendsto.subseq_mem, WithVal.strictMono_valueGroupOrderIso₀_symm, Ordinal.IsFundamentalSeq.strictMono, Submodule.finrank_strictMono, exists_seq_strictAnti_strictMono_tendsto, strictMono_of_le_iff_le, NonemptyInterval.toDualProd_strictMono, LinearOrderedAddCommGroupWithTop.sub_left_strictMono_of_ne_top, strictMono_int_of_lt_succ, Submodule.map_strictMono_of_injective, Valuation.RankOne.strictMono, strictAnti_toDual_comp_iff, CauchySeq.subseq_mem, Field.Emb.Cardinal.strictMono_leastExt, PrincipalSeg.strictMono, Real.strictMono_rpow_of_base_gt_one, StrictMono.prodMap, Finset.dens_strictMono, LinearOrderedAddCommGroupWithTop.strictMono_add_left_of_ne_top, Real.arctan_strictMono, strictMonoOn_univ, strictMono_mul_right_of_pos, Ordinal.derivFamily_strictMono, QuotientAddGroup.strictMono_comap_prod_map, Filter.Tendsto.subseq_mem_entourage, Fin.val_strictMono, List.foldl_strictMono, LowerSet.Iic_strictMono, Submodule.comap_strictMono_of_surjective, Real.exp_strictMono, ZFSet.vonNeumann_strictMono, NNReal.strictMono_rpow_of_pos, LTSeries.strictMono, Order.isNormal_iff_strictMono_and_continuous, StrictAnti.dual_left, StrictMono.codRestrict, Filter.extraction_forall_of_eventually', Nat.succPNat_strictMono, Subsemigroup.strictMono_topEquiv, OrderMonoidIso.strictMono_symm, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae, Fin.strictMono_addNat, MvPolynomial.supported_strictMono, strictMono_iff_forall_covBy, AddSubsemigroup.strictMono_topEquiv, AddSubgroup.toAddSubmonoid_strictMono, Sum.inl_strictMono, StrictMono.ite', ValuativeRel.RankLeOneStruct.strictMono, Subsemiring.toSubmonoid_strictMono, ValuationSubring.unitGroup_strictMono, Filter.extraction_of_frequently_atTop, strictMono_smul_left_of_pos, WithTop.pred_strictMono, StrictAnti.neg, Continuous.strictMonoOn_of_inj_rigidity, AddEquiv.strictMono_subsemigroupCongr, strictMono_id, Odd.strictMono_pow, pow_left_strictMono, Fin.strictMono_succ, Filter.strictMono_subseq_of_tendsto_atTop, Fin.cast_strictMono, Fin.strictMono_iff_lt_succ, Cardinal.mk_strictMono, Metric.exists_subseq_bounded_of_cauchySeq, AddSubsemigroup.comap_strictMono_of_surjective, RingHom.strictMono_specComap_of_surjective, Subring.toSubsemiring_strictMono, List.sortedLT_iff_strictMono_get, strictMono_mul_left_of_pos, zsmul_left_strictMono, Finset.nsmul_right_strictMono, Sum.Lex.inl_strictMono, zpow_left_strictMono, Subring.toAddSubgroup_strictMono, QuotientGroup.strictMono_comap_prod_image, WithBot.strictMono_iff, Finset.strictMono_iff_forall_lt_insert, TopologicalSpace.FirstCountableTopology.tendsto_subseq, PartialOrder.mem_nerve_nonDegenerate_iff_strictMono, WithVal.strictMono_valueGroupEquiv_symm, Submodule.toAddSubgroup_strictMono, Function.Injective.image_strictMono, Set.card_strictMono, Ordinal.strictMono_gamma, Fintype.sum_strictMono, SetLike.coe_strictMono, CompositionSeries.strictMono, EReal.coe_strictMono, Order.pred_strictMono, List.Sorted.get_strictMono, StrictMonoOn.strictMono, StrictMono.iterate, StrictMono.const_mul', List.SortedLT.strictMono_get, Cardinal.natCast_mul_strictMono, WithBot.strictMono_map_iff, Equiv.Set.Equiv.strictMono_setCongr, GaloisCoinsertion.strictMono_l, WellFoundedLT.rank_strictMono, Fin.strictMono_castSucc, StrictAnti.inv, StrictAnti.comp, Continuous.strictMono_of_inj, StrictMonoOn.Iic_union_Ici, Monotone.strictMono_of_injective, StrictMono.pow_const, Nat.pow_left_strictMono, Nat.fib_add_two_strictMono, Order.isNormal_iff', Cardinal.ofENat_strictMono, Submodule.toSubMulAction_strictMono, hahnEmbedding_isOrderedModule_rat, Filter.HasAntitoneBasis.subbasis_with_rel, Subring.toSubmonoid_strictMono, Ordinal.omega_strictMono, Field.Emb.Cardinal.strictMono_filtration, ENNReal.mul_right_strictMono, Pi.toColex_strictMono, Pi.mulSingle_strictMono, Monotone.mul_strictMono', Real.arsinh_strictMono, InitialSeg.strictMono, Filter.strictMono_subseq_of_id_le, Ordinal.IsNormal.strictMono, strictMono_restrict, StrictAnti.dual_right, OrderMonoidIso.strictMono, ack_strictMono_right, StrictMono.dual, WithTop.coe_strictMono, ProbabilityTheory.Fernique.normThreshold_strictMono, Pell.strictMono_x, Equiv.image_strictMono, StrictMonoOn.restrict, CauchySeq.subseq_subseq_mem, Cardinal.beth_strictMono, strictMono_of_pred_lt, Rat.cast_strictMono, Int.exists_strictMono, AddSubgroup.ofAddUnits_strictMono, List.sorted_lt_ofFn_iff, Nat.strictMono_cast, ENat.mul_left_strictMono, Subsemigroup.map_strictMono_of_injective, MonoidHom.inl_strictMono, Real.sin_arctan_strictMono, Tuple.eq_sort_iff', DyckWord.strictMono_semilength, Ordinal.preOmega_strictMono, WithZeroMulInt.toNNReal_strictMono, StrictMono.strictMono_iterate_of_lt_map, Finset.Colex.toColex_image_ofColex_strictMono, Multiset.map_strictMono, PNat.natPred_strictMono, toWellOrderExtension_strictMono, List.SortedLT.strictMono, UpperSet.Ioi_strictMono, StrictMono.add_const, Fin.strictMono_castAdd, MonoidHom.inr_strictMono, MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff, Order.isNormal_iff, Prod.Lex.toLex_strictMono, exists_seq_strictMono_tendsto, Continuous.strictMono_of_inj_boundedOrder, Cardinal.ord_strictMono, Real.sinh_strictMono, Ideal.matrix_strictMono_of_nonempty, Metric.exists_subseq_summable_dist_of_cauchySeq, AddConstMapClass.strictMono_iff_Icc, LocallyFiniteOrder.orderMonoidHom_strictMono, ENat.strictMono_map_iff, mulintEquivOfZPowersEqTop_strictMono, Nat.fermatNumber_strictMono, strictMono_div_right_of_pos, AddSubmonoid.map_strictMono_of_injective, MonoidWithZeroHom.inr_strictMono, ENNReal.coe_strictMono, strictMono_vecCons, Int.natCast_strictMono, OrderedFinpartition.parts_strictMono, EReal.coe_ennreal_strictMono, OrderAddMonoidIso.strictMono, NonUnitalSubring.toAddSubgroup_strictMono, Polynomial.Sequence.degree_strictMono, AddSubsemigroup.map_strictMono_of_injective, SSet.prodStdSimplex.strictMono_orderHomOfSimplex, strictMono_smul_right_of_pos, StrictMono.mul_monotone, StrictAnti.mul_const_of_neg, Finset.strictMono_iff_forall_lt_cons, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, Subsemiring.toAddSubmonoid_strictMono, Subsingleton.strictMono, WithTop.mul_left_strictMono, IntermediateField.toSubalgebra_strictMono, Cardinal.preBeth_strictMono, Ordinal.veblen_right_strictMono, GradeOrder.grade_strictMono, Sum.inr_strictMono, nsmul_right_strictMono, Set.range_injOn_strictMono, Monotone.add_strictMono, OrderedFinpartition.emb_strictMono, IsLocalization.coeSubmodule_strictMono, LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top, IsLUB.exists_seq_strictMono_tendsto_of_notMem, Fin.strictMono_castLE, StrictMono.comp, zpow_right_strictMono₀, smul_strictMono_right, HahnEmbedding.Partial.sSupFun_strictMono, StrictMono.add, Concept.strictMono_extent, Order.IsNormal.strictMono, WithTop.strictMono_iff, Finset.disjSum_strictMono_right, Pi.single_strictMono, List.sortedLT_ofFn_iff, ENNReal.strictMono_rpow_of_pos, Fintype.prod_strictMono', Cardinal.lift_strictMono, Multiset.powerset_strictMono, Dense.exists_seq_strictMono_tendsto_of_lt, LocallyFiniteOrder.orderMonoidWithZeroHom_strictMono, strictMono_inf_prod_sup, Sum.Lex.toLex_strictMono, Dense.exists_seq_strictMono_tendsto, AddMonoidHom.inr_strictMono, strictMono_iff_map_neg, Finset.strictMono_sym2, Polynomial.Sequence.basis_degree_strictMono, WithBot.succ_strictMono, exists_seq_strictMono_tendsto', pow_right_strictMono', Subsemigroup.comap_strictMono_of_surjective, Finset.pow_right_strictMono, tendsto_subseq_of_bounded, CategoryTheory.isNoetherianObject_iff_not_strictMono, WithVal.strictMono_valueGroupEquiv, StrictMono.mul_const, Submonoid.map_strictMono_of_injective, Multiset.disjSum_strictMono_right, ENat.mul_right_strictMono, QuotientGroup.strictMono_comap_prod_map, Valuation.RankLeOne.strictMono', DivisorChain.exists_chain_of_prime_pow, CompactSpace.tendsto_subseq, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, StrictAnti.const_mul_of_neg, ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, strictMono_toDual_comp_iff, Module.Basis.flag_strictMono, WithTop.mul_right_strictMono, Pell.IsFundamental.y_strictMono, Archimedean.embedRealFun_strictMono, nsmul_left_strictMono, NonUnitalSubring.toSubsemigroup_strictMono, Set.ncard_strictMono, zsmul_strictMono_right, Nat.exists_strictMono_subsequence, Real.sigmoid_strictMono, StrictMono.mul_monotone', LinearPMap.domain_mono, Multiset.toFinsupp_strictMono, MonoidWithZeroHom.ValueGroup₀.embedding_strictMono, tendsto_subseq_of_frequently_bounded, pow_right_strictMono₀, FirstOrder.Language.HomClass.strictMono, Ordinal.veblen_zero_strictMono, Real.exists_seq_rat_strictMono_tendsto, WithZero.toMulBot_strictMono, TwoSidedIdeal.matrix_strictMono_of_nonempty, FractionalIdeal.mul_right_strictMono, StrictMono.nat_pow, strictAnti_comp_ofDual_iff, Pi.toLex_strictMono, Subtype.strictMono_coe, mul_left_strictMono, StrictMono.mul_const', WithBot.coe_strictMono, AddEquiv.strictMono_symm, Ordinal.enumOrd_strictMono, Finsupp.Colex.single_strictMono, Ordinal.eq_enumOrd, WithZero.withZeroUnitsEquiv_strictMono, Multiset.card_strictMono, IsCompact.tendsto_subseq, arithGeom_strictMono, ENNReal.mul_left_strictMono, StrictMono.withTop_map, FirstOrder.Language.Substructure.map_strictMono_of_injective, Fin.strictMono_natAdd, hahnEmbedding_isOrderedModule, Set.strictMonoOn_iff_strictMono, UpperSet.Ici_strictMono
|
StrictMonoOn 📖 | MathDef | 101 mathmath: Nat.pow_self_strictMonoOn, Function.locallyFinsuppWithin.logCounting_strictMono, strictAntiOn_toDual_comp_iff, Set.Finite.ecard_strictMonoOn, StrictMonoOn.congr, Real.strictMonoOn_sqrt, StrictAntiOn.dual_left, strictAntiOn_comp_ofDual_iff, StrictMonoOn.comp, StrictMonoOn.union, strictMonoOn_of_lt_add_one, Set.strictMonoOn_projIic, StrictMonoOn.mul_monotone', StrictConvexOn.strictMonoOn_deriv, StrictAntiOn.neg, ConvexOn.strict_mono_of_lt, Set.Subsingleton.strictMonoOn, strictMonoOn_id, Real.strictMonoOn_artanh, StrictAntiOn.comp, Finset.pow_right_strictMonoOn, strictMonoOn_dual_iff, StrictMono.of_restrict, sup_strictMonoOn_Icc_inf, upperCentralSeries.StrictMonoOn, ContinuousOn.strictMonoOn_of_injOn_Icc', Cardinal.mk_strictMonoOn, AkraBazziRecurrence.strictMonoOn_one_sub_smoothingFn, MonotoneOn.mul_strictMono', StrictAnti.comp_strictAntiOn, StrictMonoOn.add_monotone, StrictMonoOn.mono, Real.strictMonoOn_logb_of_base_lt_one, zpow_left_strictMonoOn₀, Real.Gamma_strictMonoOn_Ici, strictMonoOn_insert_iff, StrictMono.strictMonoOn_IccExtend, ContinuousOn.strictMonoOn_of_injOn_Ioo, StrictMonoOn.add, Set.Finite.card_strictMonoOn, StrictMonoOn.mul_const', strictMonoOn_of_hasDerivWithinAt_pos, MonotoneOn.strictMonoOn_of_injOn, strictMonoOn_univ, StrictMono.strictMonoOn_IciExtend, strictMonoOn_mul_self, Cardinal.toNat_strictMonoOn, StrictConvexOn.strictMonoOn_derivWithin, strictMonoOn_insert_iff_of_forall_ge, ContinuousOn.strictMonoOn_of_injOn_Icc, strictMonoOn_toDual_comp_iff, MonotoneOn.add_strictMono, StrictMonoOn.add_const, Set.strictMonoOn_projIcc, Real.strictMonoOn_logb, StrictMonoOn.const_mul', StrictMono.strictMonoOn_IicExtend, strictMonoOn_insert_iff_of_forall_le, Cardinal.toENat_strictMonoOn, Real.qaryEntropy_strictMonoOn, Real.strictMonoOn_arcsin, ConvexOn.strictMonoOn, Real.strictMonoOn_arcosh, Nat.fib_strictMonoOn, Set.strictMonoOn_projIci, StrictMonoOn.mul', StrictMono.comp_strictMonoOn, eVariationOn.eVariationOn_eq_strictMonoOn, ConcaveOn.strictMonoOn, MonotoneOn.strictMonoOn_iff_injOn, StrictMono.strictMonoOn, strictMono_restrict, Real.cosh_strictMonoOn, strictMonoOn_of_pred_lt, Real.strictMonoOn_one_add_div_one_sub, Real.strictMonoOn_log, Nat.nth_strictMonoOn, strictMonoOn_of_lt_succ, Set.strictMonoOn_singleton, AddConstMapClass.strictMono_iff_Icc, strictMonoOn_of_deriv_pos, pow_left_strictMonoOn₀, inf_strictMonoOn_Icc_sup, Int.strictMonoOn_natAbs, Set.Finite.ncard_strictMonoOn, Real.strictMonoOn_sin, Real.strictMonoOn_tan, Real.strictMonoOn_rpow_Ici_of_exponent_pos, strictMonoOn_comp_ofDual_iff, StrictMonoOn.dual, Set.Finite.encard_strictMonoOn, strictMonoOn_Iic_of_lt_succ, Set.EqOn.congr_strictMonoOn, strictMonoOn_Ici_of_pred_lt, StrictMonoOn.const_add, StrictAntiOn.dual_right, strictMonoOn_of_sub_one_lt, StrictAntiOn.inv, Finset.nsmul_right_strictMonoOn, Real.binEntropy_strictMonoOn, Set.strictMonoOn_iff_strictMono
|
instDecidableAntitoneOfForallForallForallLe 📖 | CompOp | — |
instDecidableAntitoneOnOfForallForallMemSetForallForallForallLe 📖 | CompOp | — |
instDecidableMonotoneOfForallForallForallLe 📖 | CompOp | — |
instDecidableMonotoneOnOfForallForallMemSetForallForallForallLe 📖 | CompOp | — |
instDecidableStrictAntiOfForallForallForallLt 📖 | CompOp | — |
instDecidableStrictAntiOnOfForallForallMemSetForallForallForallLt 📖 | CompOp | — |
instDecidableStrictMonoOfForallForallForallLt 📖 | CompOp | — |
instDecidableStrictMonoOnOfForallForallMemSetForallForallForallLt 📖 | CompOp | — |