| Name | Category | Theorems |
|---|
Antitone 📖 | MathDef | 171 mathmath: seminormFromConst_seq_antitone, fixingSubgroup_antitone, Dynamics.coverEntropyInfEntourage_antitone, not_monotone_not_antitone_iff_exists_le_le, Monotone.mul_const_of_nonpos, MeasureTheory.GridLines.T_lmarginal_antitone, zpow_right_anti₀, antitone_continuousOn, ArchimedeanClass.addSubgroup_antitone, lowerPolar_anti, antitone_mul_left, Monotone.Ici, Subsingleton.antitone', LinearMap.polar_antitone, lowerCentralSeries_antitone, 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, antitone_Ioi, Set.antitoneOn_iff_antitone, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map, Dynamics.netEntropyEntourage_antitone, compl_anti, antitone_le, derivedSeries_antitone, MeasureTheory.hittingBtwn_apply_anti, antitone_add_nat_iff_antitoneOn_nat_Ici, Stirling.stirlingSeq'_antitone, antitone_toDual_comp_iff, StrictMono.trans_antivary, antitone_iff_map_nonpos, IntermediateField.fixedField_antitone, Dynamics.coverMincard_antitone, monotone_toDual_comp_iff, Dynamics.netMaxcard_antitone, AlgebraicGeometry.Scheme.IdealSheafData.support_antitone, Order.PFilter.antitone_principal, Finsupp.DegLex.single_antitone, t1Space_antitone, Matrix.IsHermitian.eigenvalues₀_antitone, antitone_of_odd_of_monotoneOn_nonneg, Monotone.dual_left, Real.antitone_arccos, 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, antitone_iff_forall_lt', 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, MulArchimedeanClass.ballSubgroup_antitone, IntermediateField.fixingSubgroup_antitone, 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_dual_iff, Set.antitone_bforall, ArchimedeanClass.ballAddSubgroup_antitone, antitone_of_deriv_nonpos, Dynamics.coverEntropyInf_antitone, antitone_smul_left, Monotone.dual_right, antitone_int_of_succ_le, List.SortedGE.antitone, Monotone.inv, AffineMap.lineMap_anti, antitone_add_nat_of_succ_le, isLowerSet_setOf, NNReal.agmSequences_monotone_and_antitone, Monotone.neg, Stirling.log_stirlingSeq'_antitone, CategoryTheory.Triangulated.TStructure.ge_antitone, MeasureTheory.Egorov.notConvergentSeq_antitone, antitone_nat_of_succ_le, antitone_iff_apply₂, Finset.sum_anti_set_of_nonpos, antitone_mul_right, 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, fixedPoints_subgroup_antitone, fixingAddSubmonoid_antitone, fixedPoints_antitone_addSubmonoid, CategoryTheory.MorphismProperty.antitone_llp, SimpleGraph.egirth_anti, PairReduction.antitone_logSizeBallSeq_add_one_subset, MulArchimedeanClass.subgroup_antitone, List.sorted_ge_ofFn_iff, 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, Filter.IsAntitoneBasis.antitone, List.sortedGE_iff_antitone_get, NNReal.agmSequences_snd_antitone, List.SortedGE.antitone_get, Subsingleton.antitone, antitone_iff_forall_lt, isClosed_antitone, antitone_const, Filter.HasAntitoneBasis.antitone, antitone_comp_ofDual_iff, Order.coheight_anti, exists_seq_tendsto_sInf, one_div_pow_anti, 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, not_monotone_not_antitone_iff_exists_lt_lt, antitone_of_succ_le, fixedPoints_antitone, Finset.prod_anti_set_of_le_one, antitone_vecEmpty, MeasureTheory.hittingAfter_anti, Antivary.exists_monotone_antitone, ArchimedeanClass.ball_antitone, List.sortedGE_ofFn_iff, integral_sin_pow_antitone, Finset.antitone_iff_forall_cons_le, EReal.antitone_div_right_of_nonpos, antivary_iff_exists_antitone_monotone, LinearMap.IsSymmetric.eigenvalues_antitone, Monovary.exists_antitone, StrictAnti.antitone, BoxIntegral.Box.antitone_lower, upperClosure_anti, leOnePart_anti
|
AntitoneOn 📖 | MathDef | 75 mathmath: Set.Subsingleton.antitoneOn, MonotoneOn.dual_left, 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, Real.antitoneOn_cos, Set.antitoneOn_iff_antitone, AntivaryOn.exists_antitoneOn_monotoneOn, ConcaveOn.antitoneOn_slope_gt, Set.EqOn.congr_antitoneOn, Nat.clog_antitone_left, antitone_add_nat_iff_antitoneOn_nat_Ici, MonotoneOn.Ici, 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, antivaryOn_iff_exists_monotoneOn_antitoneOn, Nat.log_antitone_left, MulArchimedeanClass.mk_antitoneOn, AddConstMapClass.antitone_iff_Icc, Real.log_div_self_antitoneOn, antitoneOn_nat_Ici_of_succ_le, antitoneOn_comp_ofDual_iff, Real.log_div_sqrt_antitoneOn, antitoneOn_of_succ_le, inv_antitoneOn_Icc_right, MonotoneOn.inv, monotoneOn_toDual_comp_iff, antitoneOn_univ, AntitoneOn.of_map_inf, QuasilinearOn.monotoneOn_or_antitoneOn, antitoneOn_dual_iff, antitoneOn_of_add_one_le, dist_anti_right_pi, AntivaryOn.exists_monotoneOn_antitoneOn, antivaryOn_id_iff, MonotoneOn.dual_right, Antitone.comp_monotoneOn, StrictAntiOn.antitoneOn, ConcaveOn.antitoneOn_derivWithin, Set.antitoneOn_insert_iff, sub_inv_antitoneOn_Icc_right, inv_antitoneOn_Ioi, MonovaryOn.exists_antitoneOn, Real.antitoneOn_rpow_Ioi_of_exponent_nonpos, StrictMonoOn.trans_antivaryOn, antivaryOn_iff_exists_antitoneOn_monotoneOn, Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt, antitoneOn_of_deriv_nonpos, 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, inv_antitoneOn_Icc_left, antitoneOn_iff_forall_lt', inv_antitoneOn_Iio, dist_anti_left_pi
|
MonotoneOn 📖 | MathDef | 83 mathmath: Antitone.comp_antitoneOn, 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, AntitoneOn.neg, Real.log_mul_self_monotoneOn, MonovaryOn.exists_monotoneOn, monotoneOn_comp_ofDual_iff, ConvexOn.monotoneOn_rightDeriv, quasilinearOn_iff_monotoneOn_or_antitoneOn, Real.monotoneOn_posLog, monotone_add_nat_iff_monotoneOn_nat_Ici, MonotoneOn.of_map_sup, monotoneOn_descPochhammer_eval, AntivaryOn.exists_antitoneOn_monotoneOn, StrictAntiOn.trans_antivaryOn, Cardinal.toNat_monotoneOn, ArchimedeanClass.mk_monotoneOn, 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_const, ConvexOn.monotoneOn_deriv, MulArchimedeanClass.mk_monotoneOn, CFC.log_monotoneOn, CFC.monotoneOn_one_sub_one_add_inv_real, AntitoneOn.Ioi, pow_left_monotoneOn, dist_mono_left_pi, monotoneOn_iff_forall_lt', StrictMonoOn.trans_monovaryOn, ConvexOn.slope_mono, ArchimedeanClass.stdPart_monotoneOn, AddConstMapClass.monotone_iff_Icc, antitoneOn_comp_ofDual_iff, AntitoneOn.dual_left, monotoneOn_of_le_succ, ConvexOn.monotoneOn_leftDeriv, variationOnFromTo.sub_self_monotoneOn, AntitoneOn.inv, AntitoneOn.comp, Nat.pow_monotoneOn, Set.Subsingleton.monotoneOn, Set.monotoneOn_singleton, monotoneOn_toDual_comp_iff, monotoneOn_id, LocallyBoundedVariationOn.exists_monotoneOn_sub_monotoneOn, StrictMonoOn.monotoneOn, QuasilinearOn.monotoneOn_or_antitoneOn, monotoneOn_of_pred_le, variationOnFromTo.monotoneOn, Function.locallyFinsuppWithin.logCounting_mono, monovaryOn_id_iff, AntivaryOn.exists_monotoneOn_antitoneOn, Real.monotoneOn_sin, ConvexOn.monotoneOn_derivWithin, ConvexOn.monotoneOn_slope_gt, antivaryOn_iff_exists_antitoneOn_monotoneOn, dist_mono_right_pi, Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt, Set.monotoneOn_insert_iff, Monotone.monotoneOn, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, monotoneOn_dual_iff, zpow_left_monoOn₀, Set.EqOn.congr_monotoneOn, isClosed_monotoneOn, ValueDistribution.logCounting_monotoneOn, monotoneOn_univ
|
StrictAnti 📖 | MathDef | 96 mathmath: zpow_right_strictAnti, Continuous.strictMono_of_inj_boundedOrder', StrictMono.strictAnti_iterate_of_map_lt, Nat.exists_strictAnti', unitInterval.strictAnti_symm, one_div_pow_strictAnti, exists_seq_strictAnti_tendsto', strictAnti_vecEmpty, StrictMono.neg, EReal.neg_strictAnti, exists_seq_strictAnti_tendsto, strictAnti_mul_right, CategoryTheory.isArtinianObject_iff_not_strictAnti, Finsupp.Lex.single_strictAnti, inv_pow_strictAnti, List.SortedGT.strictAnti, StrictMono.dual_right, StrictMono.const_mul_of_neg, MulArchimedeanClass.subsemigroup_strictAnti, 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, 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, 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, strictAnti_iff_map_pos, zsmul_left_strictAnti, AddConstMapClass.strictAnti_iff_Icc, pow_right_strictAnti₀, List.sortedGT_ofFn_iff, WithTop.strictAnti_iff, strictAnti_of_deriv_neg, strictAnti_dual_iff, Continuous.strictMono_of_inj, compl_strictAnti, Concept.strictAnti_intent, strictAnti_int_of_succ_lt, StrictMono.mul_const_of_neg, 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, FiniteMulArchimedeanClass.subgroup_strictAnti, DenseRange.exists_seq_strictAnti_tendsto_of_lt, strictMono_toDual_comp_iff, Set.strictAntiOn_iff_strictAnti, strictAnti_of_lt_pred, Nat.exists_strictAnti, 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 | 55 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, Real.Gamma_strictAntiOn_Ioc, inv_strictAntiOn, one_div_strictAntiOn, StrictMonoOn.dual_left, StrictMonoOn.neg, ContinuousOn.strictMonoOn_of_injOn_Icc', Set.EqOn.congr_strictAntiOn, Polynomial.Chebyshev.strictAntiOn_node, 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_of_succ_lt, AddConstMapClass.strictAnti_iff_Icc, ConvexOn.strictAntiOn, Real.strictAntiOn_logb_of_base_lt_one, 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_univ, strictAntiOn_Iic_of_succ_lt, strictAntiOn_of_hasDerivWithinAt_neg, Real.strictAntiOn_cos, strictAntiOn_Ici_of_lt_pred, Real.binEntropy_strictAntiOn, AntitoneOn.strictAntiOn_of_injOn, strictAntiOn_insert_iff_of_forall_le, ConcaveOn.strictAntiOn, StrictMonoOn.dual_right, strictMonoOn_comp_ofDual_iff, Set.strictAntiOn_iff_strictAnti, strictAntiOn_dual_iff, strictAntiOn_of_add_one_lt, ContinuousOn.strictAntiOn_of_injOn_Icc, AkraBazziRecurrence.strictAntiOn_smoothingFn
|
StrictMono 📖 | MathDef | 381 mathmath: Finset.val_strictMono, 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, WithBotTop.coe_strictMono, Nat.exists_strictMono, Polynomial.Sequence.basis_natDegree_strictMono, Finset.card_strictMono, Finsupp.toMultiset_strictMono, strictMono_of_hasDerivAt_pos, Filter.extraction_forall_of_frequently, IsFractionRing.coeSubmodule_strictMono, AddSubmonoid.comap_strictMono_of_surjective, Nat.exists_strictMono', 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, RingCon.matrix_strictMono_of_nonempty, Ordinal.deriv_strictMono, LowerSet.Iio_strictMono, Subgroup.ofUnits_strictMono, WithTop.pow_right_strictMono, Fin.strictMono_succAbove, OrderIso.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, 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, ENNReal.log_strictMono, HahnEmbedding.Seed.strictMono_coeff, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, DenseRange.exists_seq_strictMono_tendsto, 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, 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, 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, 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, Finset.geomSum_ofColex_strictMono, strictMono_comp_ofDual_iff, Real.strictMono_eulerMascheroniSeq, OrderEmbedding.strictMono, Filter.subseq_tendsto_of_neBot, LocallyFiniteOrder.orderAddMonoidHom_strictMono, QuotientAddGroup.strictMono_comap_prod_image, NonUnitalSubsemiring.toSubsemigroup_strictMono, WithZero.withZeroUnitsEquiv_symm_strictMono, Filter.Tendsto.subseq_mem, 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, 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, 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, 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, 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, Submodule.toAddSubgroup_strictMono, Function.Injective.image_strictMono, Ordinal.strictMono_gamma, Fintype.sum_strictMono, SetLike.coe_strictMono, CompositionSeries.strictMono, EReal.coe_strictMono, Order.pred_strictMono, List.Sorted.get_strictMono, StrictMonoOn.strictMono, 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, Nat.pow_left_strictMono, Nat.fib_add_two_strictMono, Order.isNormal_iff', Cardinal.ofENat_strictMono, Submodule.toSubMulAction_strictMono, hahnEmbedding_isOrderedModule_rat, Valuation.RankOne.strictMono', 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, Real.arsinh_strictMono, InitialSeg.strictMono, Filter.strictMono_subseq_of_id_le, Ordinal.IsNormal.strictMono, strictMono_restrict, StrictAnti.dual_right, OrderMonoidIso.strictMono, ack_strictMono_right, WithTop.coe_strictMono, ProbabilityTheory.Fernique.normThreshold_strictMono, Pell.strictMono_x, 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, Multiset.map_strictMono, PNat.natPred_strictMono, toWellOrderExtension_strictMono, List.SortedLT.strictMono, UpperSet.Ioi_strictMono, 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, 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, strictMono_smul_right_of_pos, 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, OrderedFinpartition.emb_strictMono, IsLocalization.coeSubmodule_strictMono, LinearOrderedAddCommGroupWithTop.strictMono_add_right_of_ne_top, IsLUB.exists_seq_strictMono_tendsto_of_notMem, Fin.strictMono_castLE, zpow_right_strictMono₀, smul_strictMono_right, HahnEmbedding.Partial.sSupFun_strictMono, 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, 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, Submonoid.map_strictMono_of_injective, Multiset.disjSum_strictMono_right, ENat.mul_right_strictMono, QuotientGroup.strictMono_comap_prod_map, DivisorChain.exists_chain_of_prime_pow, CompactSpace.tendsto_subseq, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, StrictAnti.const_mul_of_neg, 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, LinearPMap.domain_mono, Multiset.toFinsupp_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, strictAnti_comp_ofDual_iff, Pi.toLex_strictMono, Subtype.strictMono_coe, mul_left_strictMono, Ordinal.isNormal_iff_strictMono_and_continuous, WithBot.coe_strictMono, 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, FirstOrder.Language.Substructure.map_strictMono_of_injective, Fin.strictMono_natAdd, hahnEmbedding_isOrderedModule, Set.strictMonoOn_iff_strictMono, UpperSet.Ici_strictMono
|
StrictMonoOn 📖 | MathDef | 80 mathmath: Nat.pow_self_strictMonoOn, strictAntiOn_toDual_comp_iff, Real.strictMonoOn_sqrt, StrictAntiOn.dual_left, strictAntiOn_comp_ofDual_iff, strictMonoOn_of_lt_add_one, Set.strictMonoOn_projIic, 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, ContinuousOn.strictMonoOn_of_injOn_Icc', Cardinal.mk_strictMonoOn, AkraBazziRecurrence.strictMonoOn_one_sub_smoothingFn, StrictAnti.comp_strictAntiOn, 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_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, Set.strictMonoOn_projIcc, Real.strictMonoOn_logb, 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, 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, Set.Finite.encard_strictMonoOn, strictMonoOn_Iic_of_lt_succ, Set.EqOn.congr_strictMonoOn, strictMonoOn_Ici_of_pred_lt, 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 | — |