| Metric | Count |
|---|
DefinitionsAsLinearOrder, linearOrder, linearOrder, partialOrder, preorder, lift', liftWithOrd, liftWithOrd', ofSubsingleton, exactLeOfLt, decidable, instLinearOrder, hasLe, instCompl, partialOrder, preorder, sdiff, instDecidableLE, instLE_mathlib, instPartialOrder, instPreorder, instCompl, le, partialOrder, StrongLT, decidableLE, decidableLT, instLinearOrder, partialOrder, preorder, instInhabitedAsLinearOrder, instLinearOrderEmpty, instLinearOrderPEmpty, Β«term_β»ΒΉ'o_Β» | 34 |
Theoremseq_iff_ge_not_gt, eq_iff_le_not_lt, eq_or_lt_of_le, eq_or_lt_of_le', le_iff_eq_or_lt, le_iff_eq_or_lt', ne_iff_gt_iff_ge, ne_iff_lt_iff_le, dense, dense', ge, le, not_gt, not_lt, trans_ge, trans_gt, trans_le, trans_lt, const_le_const, const_lt_const, le, lt, ext, ext_iff, antisymm, antisymm', eq_of_not_lt, eq_of_not_lt', eq_or_lt, eq_or_lt', eq_or_lt_dec, eq_or_lt_dec', ge, ge_iff_eq, ge_iff_eq', ge_or_le, ge_or_lt, gt_or_le, le_or_ge, le_or_gt, lt_iff_ne, lt_iff_ne', lt_of_ne, lt_of_ne', lt_of_not_ge, lt_or_eq, lt_or_eq', lt_or_eq_dec, lt_or_eq_dec', lt_or_ge, not_lt_iff_eq, not_lt_iff_eq', trans, trans', trans_eq, trans_eq', trans_lt, trans_lt', trans_strongLT, asymm, false, gt, gt_or_lt, le, lt_or_gt, ne, ne', not_gt, trans, trans', trans_eq, trans_eq', trans_le, trans_le', ext, ext_lt, toPartialOrder_injective, toPartialOrder_injective_iff, ge_iff_gt, gt_or_lt, instIsEquiv_compl, le_iff_lt, lt_of_le, lt_of_le', lt_or_gt, not_ge_or_not_le, not_le_or_not_ge, instDenselyOrdered, le, max_eq, min_eq, not_lt, ext, ext_lt, toPreorder_injective, toPreorder_injective_iff, compl_apply, compl_def, le_def, lt_def, sdiff_apply, sdiff_def, ext, toLE_injective, toLE_injective_iff, mk_le_mk, le_def, lt_iff, lt_of_le_of_lt, lt_of_lt_of_le, mk_le_mk, mk_le_mk_iff_left, mk_le_mk_iff_right, mk_le_swap, mk_lt_mk, mk_lt_mk_iff_left, mk_lt_mk_iff_right, mk_lt_mk_of_le_of_lt, mk_lt_mk_of_lt_of_le, mk_lt_swap, swap_le_mk, swap_le_swap, swap_lt_mk, swap_lt_swap, compl, compl, le, lt, trans_le, instDenselyOrdered, coe_le_coe, coe_lt_coe, mk_le_mk, mk_lt_mk, const_le_elim_iff, elim_le_const_iff, elim_le_elim_iff, associative_of_commutative_of_le, commutative_of_le, compare_of_injective_eq_compareOfLessAndEq, compl_ge, compl_gt, compl_le, compl_lt, dense_or_discrete, dense_or_discrete', eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt, eq_iff_ge_not_gt, eq_iff_le_not_lt, eq_of_forall_ge_iff, eq_of_forall_gt_iff, eq_of_forall_le_iff, eq_of_forall_lt_iff, eq_of_le_of_forall_gt_imp_ge_of_dense, eq_of_le_of_forall_lt_imp_le_of_dense, eq_of_le_of_not_lt, eq_of_le_of_not_lt', eq_or_eq_or_eq_of_forall_not_lt_lt, eq_or_lt_of_le, eq_or_lt_of_le', exists_between, exists_between', exists_forall_ge_and, exists_forall_le_and, exists_ge_of_linear, exists_le_of_linear, forall_ge_iff_le, forall_ge_imp_ne_iff_lt, forall_gt_iff_le, forall_gt_imp_ge_iff_le_of_dense, forall_gt_imp_ne_iff_le, forall_le_iff_le, forall_le_imp_ne_iff_lt, forall_lt_iff_le, forall_lt_imp_le_iff_le_of_dense, forall_lt_imp_ne_iff_le, ge_trans', gt_trans', instDenselyOrderedForall, instDenselyOrderedProd, le_Prop_eq, le_iff_eq_or_lt, le_iff_eq_or_lt', le_iff_le_iff_lt_iff_lt, le_imp_eq_iff_le_imp_ge, le_imp_eq_iff_le_imp_ge', le_imp_le_iff_lt_imp_lt, le_imp_le_of_le_of_le, le_of_eq_of_le', le_of_forall_ge, le_of_forall_gt, le_of_forall_gt_imp_ge_of_dense, le_of_forall_gt_imp_ne, le_of_forall_le, le_of_forall_lt, le_of_forall_lt_imp_le_of_dense, le_of_forall_lt_imp_ne, le_of_le_of_eq', le_of_strongLT, le_of_subsingleton, le_trans', le_update_iff, le_update_self_iff, lt_iff_le_and_ne, lt_iff_le_and_ne', lt_iff_lt_of_le_iff_le, lt_iff_lt_of_le_iff_le', lt_imp_lt_of_le_imp_le, lt_imp_lt_of_le_of_le, lt_of_eq_of_lt', lt_of_forall_ge_imp_ne, lt_of_forall_le_imp_ne, lt_of_lt_of_eq', lt_of_strongLT, lt_or_gt_iff_ne', lt_or_lt_iff_ne, lt_self_iff_false, lt_trans', lt_update_self_iff, max_def_lt, max_def_lt', max_rec, max_rec', min_def_lt, min_def_lt', min_rec, min_rec', ne_iff_gt_iff_ge, ne_iff_lt_iff_le, ne_of_not_ge, ne_of_not_le, not_lt_iff_eq_or_lt, not_lt_iff_eq_or_lt', not_lt_iff_le_imp_ge, not_lt_iff_not_le_or_ge, not_lt_of_subsingleton, rel_imp_eq_of_rel_imp_le, strongLT_of_le_of_strongLT, strongLT_of_strongLT_of_le, subrelation_iff_le, update_le_iff, update_le_self_iff, update_le_update_iff, update_le_update_iff', update_lt_self_iff, update_lt_update_iff | 246 |
| Total | 280 |
| Name | Category | Theorems |
|---|
hasLe π | CompOp | 325 mathmath: CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff, Sym2.toRel_mono, AddGroupNorm.coe_le_coe, Function.const_nonpos_of_nonpos, CategoryTheory.ObjectProperty.extensionProductIter_le_of_isTriangulatedClosedβ', MeasureTheory.lintegral_def, CategoryTheory.ObjectProperty.le_limitsClosure, existsMulOfLe, Function.one_le_const_of_one_le, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, instCanonicallyOrderedAddForall, GroupNorm.le_def, CategoryTheory.ObjectProperty.IsClosedUnderKernels.kernels_le, Finsupp.coe_le_coe, Prod.rprod_le_transGen_gameAdd, le_update_self_iff, instZeroLEOneClass, CategoryTheory.ObjectProperty.le_shiftClosure, ValueDistribution.proximity_zero_mul_le, Function.one_le_const, OrderHom.mk_le_mk, CategoryTheory.ObjectProperty.le_isoClosure, BoxIntegral.Box.le_TFAE, CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le, CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iff, OrderHom.piIso_symm_apply, Seminorm.coe_le_coe, Function.extend_nonpos, single_nonpos, CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable, Set.indicator_le_indicator_of_subset, ConvexOn.univ_sSup_of_countable_affine_eq, CategoryTheory.exactFunctor_le_additiveFunctor, CategoryTheory.ObjectProperty.IsClosedUnderCokernels.cokernels_le, Monotone.comp_le_comp_left, CategoryTheory.ObjectProperty.binaryProductsClosure_le_iff, PartitionOfUnity.nonneg', SimpleGraph.Reachable.mono', thickenedIndicatorAux_mono, Fin.insertNth_le_iff, CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator, thickenedIndicatorAux_subset, Part.Fix.approx_le_fix, Prod.gameAdd_le_lex, bddBelow_range_pi, AddGroupNorm.le_def, Set.indicator_le_indicator_nonneg, Monotone.iterate_le_of_le, ValueDistribution.proximity_nonneg, lt_def, pure_le_nhds, update_le_update_iff', Fin.insertNthOrderIso_symm_apply, CategoryTheory.ObjectProperty.limitsClosure_le, CategoryTheory.ObjectProperty.isClosedUnderCokernels_iff, indicator_le_thickenedIndicatorAux, Set.mulIndicator_le_self', OrderHom.coe_le_coe, Sum.one_le_elim_iff, Sym2.fromRel_mono_iff, CategoryTheory.ObjectProperty.le_extensionProduct_left, CategoryTheory.ObjectProperty.op_monotone_iff, Fin.insertNthOrderIso_toEquiv, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, Set.piecewise_mono, CategoryTheory.ObjectProperty.monotone_extensionProduct_right, BoxIntegral.Box.le_iff_bounds, bddAbove_pi, CategoryTheory.ObjectProperty.strictColimitsOfShape_monotone, CategoryTheory.ObjectProperty.colimitsOfShape_le_of_final, update_le_update_iff, MeasureTheory.SimpleFunc.coe_le, collapse_nonneg, CategoryTheory.Localization.LeftBousfield.le_W_iff, TopologicalSpace.le_def, CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le', CategoryTheory.ObjectProperty.le_extensionProductIter, Function.const_le_one_of_le_one, SimpleGraph.cliqueSet_mono', ConvexOn.sSup_of_countable_affine_eq, Function.locallyFinsuppWithin.le_def, CategoryTheory.ObjectProperty.monotone_retractClosure, CategoryTheory.isCardinalPresentable_monotone, Set.indicator_nonpos_le_indicator, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, Sum.nonneg_elim_iff, Function.const_nonneg_of_nonneg, CategoryTheory.ObjectProperty.strictLimitsOfShape_le_limitsOfShape, AlgebraicGeometry.etale_le_weaklyEtale, PseudoMetric.coe_le_coe, ValueDistribution.proximity_sum_top_le, Sum.elim_le_const_iff, CircleDeg1Lift.iterate_mono, Finset.piecewise_le_piecewise', Ordinal.IsNormal.id_le, Sym2.fromRelOrderIso_apply, CategoryTheory.ObjectProperty.ofObj_le_iff, AlgebraicGeometry.IsLocalIso.le_of_isLocalAtSource, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, CategoryTheory.ObjectProperty.le_strictLimitsClosureStep, MeasureTheory.exists_measurable_le_forall_setLIntegral_eq, Monotone.iterate_comp_le_of_le, CategoryTheory.leftExactFunctor_le_additiveFunctor, exists_continuous_nonneg_pos, MeasureTheory.SimpleFunc.mk_le_mk, Function.const_le_one, Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg, disjointed_le_id, ConvexOn.real_univ_sSup_of_countable_affine_eq, ValueDistribution.proximity_mul_zero_le, Fin.cons_le_cons, CategoryTheory.ObjectProperty.strictLimitsClosureIter_le_limitsClosure, Seminorm.bddAbove_iff, Ideal.pi_le_pi_iff, CategoryTheory.ObjectProperty.extensionProductIter_le_of_isTriangulatedClosedβ, OrderIso.funUnique_toEquiv, indicator_le_thickenedIndicator, ValueDistribution.proximity_add_top_le, isGLB_pi, CategoryTheory.GrothendieckTopology.le_def, Set.indicator_le_self', CategoryTheory.ObjectProperty.shiftClosure_le_iff, CategoryTheory.ObjectProperty.strictLimitsClosureStep_monotone, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, subrelation_iff_le, ConvexOn.sSup_of_nat_affine_eq, CategoryTheory.ObjectProperty.strictLimitsOfShape_monotone, Set.piecewise_le, Function.const_nonpos, Function.iterate_le_id_of_le_id, DFinsupp.coe_orderEmbeddingToFun, Sum.elim_le_one_iff, one_le_mulSingle, extend_partialOrder, Fin.snocOrderIso_apply, BoxIntegral.Prepartition.upper_le_upper, Set.le_mulIndicator, GroupNorm.coe_le_coe, exists_countable_upperSemicontinuous_isGLB, Relation.cutExpand_le_invImage_lex, conjneg_nonpos, RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, Fin.cons_le, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.le_isLocal_iff, CategoryTheory.ObjectProperty.monotone_isoClosure, BumpCovering.nonneg', ValueDistribution.proximity_mul_top_le, CategoryTheory.ObjectProperty.isoClosure_le_iff, NonarchAddGroupNorm.le_def, Fin.snocOrderIso_symm_apply, instCanonicallyOrderedMulForall, Finsupp.orderEmbeddingToFun_apply, Fin.consOrderIso_apply, CategoryTheory.ObjectProperty.strictMap_le_map, MeasureTheory.SimpleFunc.coe_le_coe, IsOpen.measure_eq_biSup_integral_continuous, CategoryTheory.ObjectProperty.le_isLocal_isLocal, AddGroupSeminorm.coe_le_coe, CategoryTheory.ObjectProperty.extensionProduct_le_of_isTriangulatedClosedβ, CategoryTheory.ObjectProperty.monotone_shiftClosure, CategoryTheory.ObjectProperty.le_isColocal_iff, ConvexOn.real_univ_sSup_affine_eq, mulSingle_le_one, Set.le_indicator, seminormFromBounded_nonneg, Function.one_le_extend, CategoryTheory.ObjectProperty.monotone_extensionProduct_left, disjointed_le, le_update_iff, Matrix.zero_le_one_row, thickenedIndicator_subset, Finset.piecewise_le_of_le_of_le, CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le, Ordinal.enumOrd_le_of_subset, Function.extend_le_one, bddAbove_range_pi, Set.mulIndicator_mono, Fin.consOrderIso_symm_apply, CategoryTheory.ObjectProperty.le_colimitsClosure, iSupIndep.le_iff_eq_of_iSup_eq_top, CategoryTheory.ObjectProperty.retractClosure_le_iff, Set.indicator_le_self, CategoryTheory.ObjectProperty.op_monotone, OrderIso.funUnique_apply, CategoryTheory.ObjectProperty.strictMap_monotone, SzemerediRegularity.le_stepBound, MeasurableSpace.le_def, CategoryTheory.ObjectProperty.extensionProduct_le_of_isTriangulatedClosedβ', CategoryTheory.ObjectProperty.unop_monotone_iff, gauge_mono, ConvexOn.univ_sSup_affine_eq, ConvexOn.real_univ_sSup_of_nat_affine_eq, update_le_iff, CategoryTheory.ObjectProperty.colimitsOfShape_monotone, CategoryTheory.ObjectProperty.map_monotone, Sum.elim_le_elim_iff, CategoryTheory.ObjectProperty.IsStableUnderShiftBy.le_shift, Part.Fix.le_f_of_mem_approx, ConvexOn.real_sSup_of_countable_affine_eq, BoxIntegral.Box.lower_le_upper, CategoryTheory.Triangulated.TStructure.le_zero_le, NonarchAddGroupNorm.coe_le_coe, CategoryTheory.ObjectProperty.le_def, Finset.le_piecewise_of_le_of_le, le_of_strongLT, MeasureTheory.Measure.ae_le_pi, Fin.insertNthOrderIso_apply, Fin.consOrderIso_toEquiv, orderedSub, CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy, IsWellFounded.exists_well_order_ge, CategoryTheory.ObjectProperty.limitsOfShape_monotone, Set.mulIndicator_le', Nucleus.coe_le_coe, single_nonneg, Fintype.exists_disjointed_le, Monotone.le_iterate_of_le, CategoryTheory.exactFunctor_le_leftExactFunctor, Sum.const_le_elim_iff, GroupSeminorm.coe_le_coe, CategoryTheory.ObjectProperty.extensionProductIter_retractClosure_le, Set.indicator_le, Function.const_le_const, bddBelow_pi, AddGroupSeminorm.le_def, CategoryTheory.ObjectProperty.monotone_extensionProductIter, Ideal.coe_piOrderIso_symm_apply, GroupSeminorm.le_def, AEMeasurable.exists_measurable_nonneg, Function.const_nonneg, CategoryTheory.ObjectProperty.colimitsClosure_le, DFinsupp.coe_le_coe, Part.Fix.approx_mono', HasOuterApproxClosed.indicator_le_apprSeq, StrictMono.id_le, MeasureTheory.lmarginal_le_of_subset, IsCompact.measure_eq_biInf_integral_hasCompactSupport, Function.extend_nonneg, NonarchAddGroupSeminorm.le_def, Monotone.le_iterate_comp_of_le, CategoryTheory.ObjectProperty.le_isColocal_isColocal, HomotopicalAlgebra.bifibrantObjects_le_fibrantObject, Ordinal.id_le_enumOrd, conjneg_nonneg, Fin.snocOrderIso_toEquiv, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, Sym2.toRel_mono_iff, MeasureTheory.exists_measurable_le_lintegral_eq, OrderIso.funUnique_symm_apply, Fin.le_cons, CategoryTheory.ObjectProperty.singleton_le_iff, Set.indicator_le', CategoryTheory.ObjectProperty.le_ind, CategoryTheory.ObjectProperty.unop_monotone, CategoryTheory.ObjectProperty.colimitsClosure_monotone, le_partialSups, Set.le_piecewise, ValueDistribution.proximity_top_mul_le, le_def, existsAddOfLe, StrictMono.le_id, Fin.le_insertNth_iff, exists_countable_lowerSemicontinuous_isLUB, OrderHom.piIso_apply, CategoryTheory.ObjectProperty.isClosedUnderKernels_iff, update_le_self_iff, Part.fix_le, Set.mulIndicator_le_mulIndicator_of_subset, NonarchAddGroupSeminorm.coe_le_coe, CategoryTheory.ObjectProperty.extensionProduct_retractClosure_retractClosure_le, Sym2.fromRelOrderIso_symm_apply_coe, MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable, CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.limitsOfShape_le, CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial, CategoryTheory.ObjectProperty.monotone'_extensionProductIter, CategoryTheory.ObjectProperty.le_extensionProduct_right, SimpleGraph.adj_le_reachable, CategoryTheory.Triangulated.TStructure.ge_one_le, CategoryTheory.ObjectProperty.strictColimitsOfShape_le_colimitsOfShape, ConvexOn.exists_affine_le_of_lt, BumpCovering.le_one', HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject, CategoryTheory.rightExactFunctor_le_additiveFunctor, ConvexOn.real_sSup_of_nat_affine_eq, isLUB_pi, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff, Fin.tuple0_le, InfHom.mk_le_mk, MeasurableSpace.DynkinSystem.le_def, MeasureTheory.exists_measurable_le_withDensity_eq, Set.mulIndicator_le, CategoryTheory.ObjectProperty.le_retractClosure, Finset.piecewise_le_piecewise, CategoryTheory.Pretopology.le_def, CategoryTheory.ObjectProperty.le_isLocal_W, CategoryTheory.exactFunctor_le_rightExactFunctor, CategoryTheory.ObjectProperty.isEquivalence_ΞΉOfLE_iff, Ideal.coe_piOrderIso_apply, single_le_single, Set.indicator_mono, ConvexOn.sSup_affine_eq, CategoryTheory.ObjectProperty.le_strictLimitsClosureIter, wellQuasiOrderedLE, SupHom.mk_le_mk, ConvexOn.real_sSup_affine_eq, CategoryTheory.ObjectProperty.limitsClosure_monotone, ConvexOn.univ_sSup_of_nat_affine_eq, CategoryTheory.ObjectProperty.colimitsCardinalClosure_le, Sum.elim_nonpos_iff, mulSingle_le_mulSingle, seminormFromConst_seq_nonneg, Part.Fix.approx_mono, CategoryTheory.ObjectProperty.le_colimitsCardinalClosure, MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton, MeasureTheory.lmarginal_mono, DFinsupp.orderEmbeddingToFun_apply, CategoryTheory.ObjectProperty.essSurj_ΞΉOfLE_iff, CategoryTheory.ObjectProperty.le_shift, StrongLT.le, Function.id_le_iterate_of_id_le, thickenedIndicator_mono, Set.mulIndicator_le_self, BoxIntegral.Prepartition.lower_le_lower
|
instCompl π | CompOp | 30 mathmath: compl_le, isAntichain_union, MeasureTheory.ae_eq_set_compl, CategoryTheory.Limits.kernelForkBiproductToSubtype_cone, compl_def, Std.Irrefl.compl, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit, MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq, MeasureTheory.ae_eq_set_compl_compl, Std.Refl.compl, CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom, Symmetric.compl, RelIso.compl_apply, antisymmRel_compl_apply, compl_ge, Relation.cutExpand_le_invImage_lex, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom, RelIso.compl_symm_apply, incompRel_compl_apply, SimpleGraph.cliqueFreeOn_two, antisymmRel_compl, Ne.instIsEquiv_compl, compl_lt, compl_apply, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone, incompRel_compl, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv, compl_gt, CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit, CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv
|
partialOrder π | CompOp | 18 mathmath: isOrderedRing, ceilDiv_def, isCoatomistic, CFC.nnrpow_map_pi, CFC.rpow_eq_rpow_pi, floorDiv_def, codisjoint_iff, isCoatomic, CFC.nnrpow_eq_nnrpow_pi, isAtomistic, CFC.rpow_map_pi, CFC.sqrt_map_pi, isCompl_iff, disjoint_iff, floorDiv_apply, ceilDiv_apply, isAtomic, instStarOrderedRing
|
preorder π | CompOp | 272 mathmath: single_mono, pi_Iio_mem_nhds, MeasureTheory.Measure.univ_pi_Ioc_ae_eq_Icc, update_lt_update_iff, OrdinalApprox.lfpApprox_mono_mid, MeasureTheory.GridLines.T_lmarginal_antitone, MeasureTheory.hittingBtwn_mono_left, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, Fin.preimage_insertNth_Icc_of_mem, partialSups_mono, MeasureTheory.SimpleFunc.coe_lt_coe, Function.monotone_eval, wcovBy_iff, Part.Fix.exists_fix_le_approx, card_Ici, toColex_monotone, Function.update_mono, Function.update_strictMono, Set.IsPWO.pi, isOrderedCancelMonoid, pi_Ioo_mem_nhds, Set.image_mulSingle_Ioo, Set.image_update_Ioo, BoxIntegral.Box.le_TFAE, DFinsupp.coe_mono, covBy_iff_exists_right_eq, one_lt_mulSingle, instPosSMulStrictMono, OrderHom.piIso_symm_apply, pi_Ico_mem_nhds', Part.toUnitMono_coe, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, pi_Iic_mem_nhds', card_Iic, CategoryTheory.Localization.LeftBousfield.galoisConnection, IsClopen.upperClosure_pi, MeasureTheory.hittingAfter_mono, GroupSeminorm.lt_def, instIsOrderBornology, orderClosedTopology', Set.image_mulSingle_Icc_right, isPWO, IsClosed.lowerClosure_pi, Function.antitone_iterate_of_le_id, Part.Fix.approx_mem_approxChain, IsClopen.lowerClosure_pi, MeasureTheory.Measure.univ_pi_Ioo_ae_eq_Icc, Part.Fix.approx_le_fix, RootPairing.Base.pos_or_neg_of_sum_smul_root_mem, pi_Ico_mem_nhds, Set.image_mulSingle_Ioo_right, lt_def, Fintype.prod_mono', Fintype.one_lt_prod_iff_of_one_le, supConvergenceClass', Set.image_update_Icc, conjneg_pos, Real.volume_Icc_pi, Set.image_update_Ico_right, Fintype.sum_mono, Finset.piecewise_mem_Icc', CategoryTheory.Triangulated.TStructure.le_monotone, Set.image_single_Icc_left, lt_of_strongLT, Set.image_update_Icc_left, Function.const_strictMono, Set.pi_univ_Ioo_subset, Set.image_single_Ioc, Real.volume_Icc_pi_toReal, instNeBotNhdsWithinIoi, card_Ioc, card_Icc, instBoundedLENhdsClass, isOrderedAddCancelMonoid, instNeBotNhdsWithinIio, isOrderedMonoid, covBy_iff_antisymmRel, Set.pi_univ_Iic, StrongLT.lt, AddGroupSeminorm.coe_lt_coe, ExpGrowth.expGrowthInf_monotone, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_of_equiv, Set.image_mulSingle_Ioo_left, NonarchAddGroupSeminorm.lt_def, Set.image_mulSingle_Icc, closure_upperClosure_comm_pi, OrderHom.pi_coe, Set.Icc_diff_pi_univ_Ioc_subset, CircleDeg1Lift.iterate_monotone, NonarchAddGroupSeminorm.coe_lt_coe, covBy_iff, card_Iio, Function.one_lt_const, instPosSMulReflectLE, Set.Icc_diff_pi_univ_Ioo_subset, pi_Ioc_mem_nhds, CategoryTheory.ObjectProperty.galoisConnection_isColocal, Set.image_mulSingle_Icc_left, antitone_lam, wellFoundedLT, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, pi_Ici_mem_nhds', Finsupp.coe_strictMono, MeasureTheory.hittingBtwn_anti, Set.image_single_Ioo_left, Set.ordConnected_pi, MeasureTheory.Measure.univ_pi_Ico_ae_eq_Icc, lt_update_self_iff, Set.image_single_Ioo_right, pi_Ioi_mem_nhds', MeasureTheory.Measure.univ_pi_Ioi_ae_eq_Ici, ΟScottContinuous_uncurry, Nucleus.coe_lt_coe, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, dist_mono_left_pi, BoxIntegral.Box.Icc_def, mem_parallelepiped_iff, GaloisConnection.dfun, Function.wellFoundedLT, instSMulPosReflectLT, Fin.preimage_insertNth_Icc_of_notMem, Fintype.sum_pos_iff_of_nonneg, instSMulPosStrictMono, Set.piecewise_mem_Icc, compact_Icc_space', BoxIntegral.Box.monotone_upper, wcovBy_iff_antisymmRel, Set.image_single_Ioo, instOrderClosedTopologyForall, OrdinalApprox.lfpApprox_mono_left, Set.image_update_Ioc_right, Fintype.sum_strictMono, Set.image_single_Icc_right, card_Ico, instPosSMulMono, isAtom_iff_eq_single, monotoneUncurry_coe, Part.fix_eq_ΟSup, MeasureTheory.monotone_lintegral, single_pos, instNoMaxOrderForallOfNonempty, pi_Iio_mem_nhds', CategoryTheory.Triangulated.TStructure.ge_antitone, wcovBy_iff_exists_left_eq, antitone_iff_applyβ, Set.pi_univ_Ioc_subset, isAtom_iff, Set.image_update_Ioc_left, Fintype.sum_neg_iff_of_nonpos, Set.image_mulSingle_Ico_left, tendstoIccClassNhdsPi, pi_Iic_mem_nhds, Part.ΟScottContinuous_toUnitMono, OrdinalApprox.gfpApprox_mono_mid, GroupNorm.lt_def, Set.image_single_Ico_left, monotoneCurry_coe, Part.Fix.le_f_of_mem_approx, RootPairing.Base.exists_root_eq_sum_int, Function.const_pos, Fin.insertNth_mem_Icc, toColex_strictMono, mulSingle_strictMono, Set.pi_univ_Ioi_subset, Function.const_mono, instBoundedGENhdsClass, instCompactIccSpaceForall, DFinsupp.coe_strictMono, MeasureTheory.Measure.univ_pi_Iio_ae_eq_Iic, Set.image_mulSingle_Ioc_right, monotone_iff_applyβ, Finsupp.coe_lt_coe, instSMulPosMono, infConvergenceClass, Finset.piecewise_mem_Icc_of_mem_of_mem, Function.const_lt_const, OrdinalApprox.gfpApprox_mono_left, covBy_iff_exists_left_eq, Monotone.of_applyβ, Set.image_single_Ico, NonarchAddGroupNorm.lt_def, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, dist_anti_right_pi, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, Set.image_update_Ico_left, Set.image_single_Icc, Part.Fix.approx_mono', instDenselyOrderedForall, OrderHom.coeFnHom_coe, Finset.piecewise_mem_Icc, Set.ordConnected_pi', GroupNorm.coe_lt_coe, Cycle.chain_mono, Set.image_single_Ioc_left, Set.pi_univ_Ici, Set.image_update_Ico, MeasureTheory.SimpleFunc.mk_lt_mk, Set.image_mulSingle_Ico_right, pi_Ici_mem_nhds, ΟScottContinuous_curry, dist_mono_right_pi, wcovBy_iff_exists_right_eq, uncurry_curry_ΟScottContinuous, pi_Ioc_mem_nhds', Part.Fix.mem_iff, infConvergenceClass', instSMulPosReflectLE, OrderHom.piIso_apply, update_lt_self_iff, AddGroupNorm.lt_def, evalOrderHom_coe, Set.piecewise_mem_Icc', Function.monotone_iterate_of_id_le, Part.fix_le, pi_Icc_mem_nhds, Set.image_update_Ioc, Set.image_single_Ico_right, pi_Ioi_mem_nhds, Set.image_update_Ioo_left, CategoryTheory.ObjectProperty.galoisConnection_isLocal, single_strictMono, Set.image_single_Ioc_right, Fintype.prod_strictMono', TorusIntegrable.function_integrable, Seminorm.coe_lt_coe, Set.image_mulSingle_Ioc, IsClosed.upperClosure_pi, Finsupp.coe_mono, AddGroupNorm.coe_lt_coe, pi_Ioo_mem_nhds', Part.fix_eq_ΟSup_of_ΟScottContinuous, pi_Icc_mem_nhds', isOrderedAddMonoid, NonarchAddGroupNorm.coe_lt_coe, MeasureTheory.upcrossingsBefore_mono, Fintype.prod_lt_one_iff_of_le_one, supConvergenceClass, DFinsupp.coe_lt_coe, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, Set.image_mulSingle_Ico, AddGroupSeminorm.lt_def, instNoMinOrderForallOfNonempty, Function.const_neg', MeasureTheory.hittingAfter_anti, Antitone.of_applyβ, Set.pi_univ_Iio_subset, closure_lowerClosure_comm_pi, mulSingle_mono, ExpGrowth.expGrowthSup_monotone, conjneg_neg', Function.const_lt_one, Set.image_mulSingle_Ioc_left, stdSimplex_subset_Icc, card_Ioo, card_Ioi, Set.image_update_Ioo_right, GroupSeminorm.coe_lt_coe, Icc_eq, OrderHom.partBind_coe, toLex_strictMono, Function.locallyFinsuppWithin.lt_def, monotone_lam, Set.image_update_Icc_right, Part.Fix.approx_mono, dist_anti_left_pi, Behrend.map_monotone, BoxIntegral.Box.antitone_lower, Set.pi_univ_Icc, isAtom_single, Set.pi_univ_Ico_subset, toLex_monotone
|
sdiff π | CompOp | 7 mathmath: symmDiff_def, symmDiff_apply, sdiff_def, Set.sigma_diff_sigma, MeasureTheory.ae_eq_set_symmDiff, sdiff_apply, MeasureTheory.ae_eq_set_diff
|
| Name | Category | Theorems |
|---|
instDecidableLE π | CompOp | 11 mathmath: SchwartzMap.norm_toLp_le_seminorm, IncidenceAlgebra.eulerChar_prod, Int.card_box, IncidenceAlgebra.zeta_prod_apply, SchwartzMap.eLpNorm_le_seminorm, Int.existsUnique_mem_box, Int.mem_box, IncidenceAlgebra.mu_prod_mu, SchwartzMap.one_add_le_sup_seminorm_apply, IncidenceAlgebra.zeta_prod_mk, IncidenceAlgebra.zeta_prod_zeta
|
instLE_mathlib π | CompOp | 121 mathmath: bddAbove_range_prod, GCongr.mk_le_mk, IncidenceAlgebra.prod_mk, LowerSet.inf_prod, LowerSet.sup_prod, IsLowerSet.prod, instCanonicallyOrderedMul, Set.sumEquiv_apply, LowerSet.prod_mono, LowerSet.prod_self_lt_prod_self, OmegaCompletePartialOrder.Chain.pair_zip_pair, DirectedOn.isCofinalFor_fst_image_prod_snd_image, LowerSet.bot_prod, instZeroLEOneClass, OrderHom.prodIso_apply, OrderIso.prodAssoc_apply, Fin.insertNthOrderIso_symm_apply, NonemptyInterval.toDualProdHom_apply, Fin.insertNthOrderIso_toEquiv, UpperSet.prod_le_prod_iff, lowerClosure_prod, orderedSub, Set.InjOn.sumElim, LowerSet.prod_mono_left, UpperSet.coe_prod, UpperSet.prod_top, UpperSet.top_prod, IsLUB.prod, bddAbove_prod, Filter.EventuallyLE.prodMap, swap_le_swap, UpperSet.Ici_prod_Ici, isTop_iff, UpperSet.prod_mono_left, isBot_iff, mk_le_swap, IsMax.prodMk, IncidenceAlgebra.prod_apply, IsMin.prodMk, instExistsMulOfLE, Sublattice.prodEquiv_toEquiv, bddBelow_prod, YoungDiagram.isLowerSet, IncidenceAlgebra.zeta_prod_apply, Sublattice.prodEquiv_apply, UpperSet.sup_prod, OrderIso.prodAssoc_symm_apply, LowerSet.disjoint_prod, Fin.snocOrderIso_apply, LowerSet.top_prod_top, isMax_iff, Ideal.idealProdEquiv_symm_apply, Fin.snocOrderIso_symm_apply, OrderIso.coe_prodComm, Filter.EventuallyLE.prodMap_nhds, LowerSet.coe_prod, Set.sumEquiv_symm_apply, Fin.consOrderIso_apply, lowerBounds_prod, isLUB_prod, upperClosure_prod, UpperSet.prod_inf, UpperSet.prod_mono, Set.ncard_sumEquiv_symm_apply, LowerSet.prod_mono_right, UpperSet.prod_self_le_prod_self, Fin.consOrderIso_symm_apply, Antisymmetrization.prodEquiv_symm_apply_mk, instExistsAddOfLE, UpperSet.prod_self_lt_prod_self, swap_le_mk, IncidenceAlgebra.one_prod_one, NumberField.InfinitePlace.bijOn_sumElim_conjugate, instCanonicallyOrderedAdd, LowerSet.prod_self_le_prod_self, LowerSet.prod_eq_bot, Finset.sumEquiv_apply_snd, Fin.insertNthOrderIso_apply, Fin.consOrderIso_toEquiv, LowerSet.prod_sup, LowerSet.prod_le_prod_iff, UpperSet.mem_prod, OrderIso.prodComm_symm, LowerSet.prod_bot, LowerSet.prod_inf_prod, IsGLB.prod, LowerSet.Iic_prod, upperBounds_prod, Fin.snocOrderIso_toEquiv, IsUpperSet.prod, UpperSet.bot_prod_bot, isMin_iff, isGLB_prod, Antisymmetrization.prodEquiv_apply_mk, LowerSet.prod_inf, OrderHom.prodIso_symm_apply, Finset.sumEquiv_apply_fst, IncidenceAlgebra.prod_mul_prod', UpperSet.prod_sup_prod, UpperSet.prod_mono_right, mk_le_mk, instWellQuasiOrderedLEProd, UpperSet.codisjoint_prod, LowerSet.mem_prod, UpperSet.inf_prod, IsTop.prodMk, le_def, mk_le_mk_iff_right, IncidenceAlgebra.prod_mul_prod, Sublattice.prodEquiv_symm_apply, IncidenceAlgebra.zeta_prod_mk, Finset.sumEquiv_symm_apply, UpperSet.prod_eq_top, IncidenceAlgebra.zeta_prod_zeta, Set.MapsTo.sumElim, UpperSet.Ici_prod, IsBot.prodMk, bddBelow_range_prod, mk_le_mk_iff_left, UpperSet.prod_sup, LowerSet.Ici_prod_Ici
|
instPartialOrder π | CompOp | 14 mathmath: instIsOrderedRingProd, instStarOrderedRing, CFC.sqrt_map_prod, Int.card_box, codisjoint_iff, CFC.rpow_map_prod, Int.existsUnique_mem_box, Int.mem_box, card_box_succ, CFC.nnrpow_eq_nnrpow_prod, disjoint_iff, isCompl_iff, CFC.rpow_eq_rpow_prod, CFC.nnrpow_map_prod
|
instPreorder π | CompOp | 221 mathmath: SchwartzMap.norm_toLp_le_seminorm, NonemptyInterval.toDualProd_mono, OrderMonoidHom.inl_mul_inr_eq_mk, mk_lt_mk_of_le_of_lt, instCompactIccSpaceProd, monotone_fst, Finset.Ioo_map_sectR, Finset.Icc_map_sectL, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, ScottContinuous.prodMk, IncidenceAlgebra.eulerChar_prod, OrderAddMonoidHom.inl_apply, cauchySeq_iff', AddMonoidHom.inl_strictMono, cauchySeq_iff_tendsto_dist_atTop_0, Finset.card_Iic_prod, OmegaCompletePartialOrder.Chain.pair_zip_pair, instIsOrderedMonoid, Filter.Tendsto.prod_map_prod_atTop, OrderAddMonoidHom.fst_comp_inl, ScottContinuousOn.snd, SSet.prodStdSimplex.objEquiv_apply_fst, Lex.toLexOrderHom_coe, OrderHom.prodIso_apply, MonoidWithZeroHom.fst_mono, OrderHom.snd_coe, Set.Iic_prod_eq, lt_of_lt_of_le, Topology.instIsLowerProd, mk_wcovBy_mk_iff_right, monotone_prod_iff, MonoidHom.inr_mono, OmegaCompletePartialOrder.Chain.zip_coe, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le, ScottContinuous.infβ, instNeBotNhdsWithinIio, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, mk_covBy_mk_iff_right, Set.IsPWO.prod, CauchySeq.prodMap, SSet.prodStdSimplex.objEquiv_Ξ΄_apply, lowerClosure_prod, OrderAddMonoidHom.addCommute_inl_inr, SSet.prodStdSimplex.objEquiv_naturality, Submodule.strictMono_comap_prod_map, Monotone.prodMk, MonoidWithZeroHom.inl_strictMono, OrderHom.prodMap_coe, instNeBotNhdsWithinIoi, wellFoundedLT, OrderMonoidHom.commute_inl_inr, SimpleGraph.hasse_prod, StrictAnti.prodMap, SSet.prodStdSimplex.objEquiv_apply_snd, monotone_prodMk_iff, Filter.prod_map_atTop_eq, wellFoundedGT', Filter.tendsto_atTop_diagonal, QuotientAddGroup.strictMono_comap_prod_image, instDenselyOrderedProd, instBoundedLENhdsClass, MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le, ScottContinuousOn.supβ, instPosSMulReflectLE, UpperSet.Ici_prod_Ici, lt_of_le_of_lt, NonemptyInterval.toDualProd_strictMono, Filter.tendsto_finset_prod_atTop, instIsOrderBornology, StrictMono.prodMap, ScottContinuous.fst, AddMonoidHom.snd_mono, OrderHom.prod_coe, noMinOrder_of_left, QuotientAddGroup.strictMono_comap_prod_map, ScottContinuousOn.fst, Finset.Ioc_map_sectL, swap_wcovBy_swap, antitone_prod_iff, OrderHom.comp_prod_comp_same, OrderHom.snd_comp_prod, AddMonoidHom.inr_mono, ScottContinuous.prod, covBy_iff, noMaxOrder_of_right, Filter.Tendsto.prod_atTop, Filter.tendsto_atBot_diagonal, ScottContinuous.fromProd, wcovBy_iff, MonoidHom.inl_mono, instIsOrderedCancelMonoid, HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp, OrderHom.prod_mono, Set.Ici_prod_eq, mk_covBy_mk_iff_left, MonoidWithZeroHom.inr_mono, swap_covBy_swap, AddMonoidHom.inl_mono, mk_lt_mk_of_lt_of_le, instIsOrderedAddCancelMonoid, QuotientGroup.strictMono_comap_prod_image, Finset.Ioo_map_sectL, SchwartzMap.eLpNorm_le_seminorm, wellFoundedGT, OrderHom.curry_apply, instInfConvergenceClassProd, SSet.prodStdSimplex.objEquiv_map_apply, swap_lt_swap, upperClosure_prod, lt_iff, Finset.Ici_prod_def, ScottContinuousOn.prodMk, Filter.instIsCountablyGeneratedAtTopProd, Monotone.prodMap, Finset.Icc_prod_def, OrderAddMonoidHom.snd_comp_inr, Antisymmetrization.prodEquiv_symm_apply_mk, instSMulPosStrictMono, Nat.pow_monotoneOn, Finset.Ioc_map_sectR, IncidenceAlgebra.one_prod_one, MonoidWithZeroHom.snd_mono, instSMulPosReflectLE, Finset.Ici_product_Ici, MonoidHom.fst_mono, OrderMonoidHom.snd_comp_inl, mk_lt_mk_iff_right, noMaxOrder_of_left, OrderMonoidHom.snd_apply, OrderMonoidHom.inl_apply, AddMonoidHom.fst_mono, Lex.toLex_mono, Topology.instIsUpperProd, Set.Icc_prod_eq, ScottContinuous.supβ, OrderHom.fst_prod_snd, OrderHom.diag_coe, OrderHom.fst_comp_prod, OrderAddMonoidHom.inr_apply, instPosSMulMono, MonoidHom.inl_strictMono, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, OrderHom.fst_coe, mk_wcovBy_mk_iff, OrderMonoidHom.fst_apply, Filter.eventually_atBot_prod_self', OrderMonoidHom.snd_comp_inr, OrderHom.curry_symm_apply, OrderAddMonoidHom.fst_comp_inr, OrderHom.prodβ_coe_coe_coe, ΟSup_snd, MonoidHom.inr_strictMono, Lex.toLex_strictMono, mk_covBy_mk_iff, supConvergenceClass, monotone_snd, MonoidWithZeroHom.inr_strictMono, Finset.Ico_map_sectR, OrderAddMonoidHom.inl_add_inr_eq_mk, ΟSupImpl_fst, Filter.prod_atTop_atTop_eq, noMinOrder_of_right, LowerSet.Iic_prod, OrderAddMonoidHom.snd_apply, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, swap_lt_mk, Antitone.prodMap, Filter.prod_atBot_atBot_eq, MonoidWithZeroHom.inl_mono, Finset.card_Ici_prod, CauchySeq.tendsto_uniformity, Finset.card_Icc_prod, Finset.Iic_product_Iic, Antisymmetrization.prodEquiv_apply_mk, OrderAddMonoidHom.snd_comp_inl, Filter.eventually_atTop_prod_self, OrderHom.prodIso_symm_apply, IncidenceAlgebra.prod_mul_prod', ScottContinuous.snd, mk_lt_mk_iff_left, Filter.prod_map_atBot_eq, cauchySeq_iff_tendsto, OrderMonoidHom.fst_comp_inr, Finset.Ico_map_sectL, instSMulPosReflectLT, Set.Ici_prod_Ici, Filter.instIsCountablyGeneratedAtBotProd, ScottContinuousOn.fromProd, ΟSup_fst, mk_lt_mk, instOrderClosedTopologyProd, Filter.Tendsto.prod_atBot, OrderMonoidHom.inr_apply, IncidenceAlgebra.mu_prod_mu, Finset.Icc_product_Icc, Set.Icc_prod_Icc, OrderAddMonoidHom.fst_apply, strictMono_inf_prod_sup, OrderMonoidHom.fst_comp_inl, AddMonoidHom.inr_strictMono, Set.Iic_prod_Iic, Finset.Iic_prod_def, mk_lt_swap, QuotientGroup.strictMono_comap_prod_map, instBoundedGENhdsClass, instIsOrderedAddMonoid, wellFoundedLT', MonoidHom.snd_mono, ΟSupImpl_snd, IncidenceAlgebra.prod_mul_prod, mk_wcovBy_mk_iff_left, SchwartzMap.one_add_le_sup_seminorm_apply, instSMulPosMono, FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop, Filter.eventually_atTop_prod_self', instPosSMulStrictMono, Finset.Icc_map_sectR, UpperSet.Ici_prod, Filter.Tendsto.prod_map_prod_atBot, Filter.eventually_atBot_prod_self, LowerSet.Ici_prod_Ici
|
| Name | Category | Theorems |
|---|
decidableLE π | CompOp | β |
decidableLT π | CompOp | 6 mathmath: HahnEmbedding.Partial.truncLT_mem_range_extendFun, HahnEmbedding.IsPartial.truncLT_mem_range, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.eval_eq_truncLT, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun
|
instLinearOrder π | CompOp | 43 mathmath: HahnEmbedding.Seed.baseEmbedding_pos, SSet.hornββ.desc.multicofork_Ο_two, SSet.hornββ.desc.multicofork_Ο_one, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Seed.baseEmbedding_strictMono, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, CategoryTheory.TransfiniteCompositionOfShape.ici_F, SSet.hornββ.desc.multicofork_pt, HahnEmbedding.Partial.extendFun_strictMono, CategoryTheory.Limits.instHasIterationOfShapeElemIic, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, HahnEmbedding.IsPartial.strictMono, unitInterval.volume_uIoo, SSet.hornββ.desc.multicofork_Ο_two_assoc, Order.IsNormal.to_Iio, SSet.hornββ.desc.multicofork_Ο_zero_assoc, Set.image_subtype_val_uIoo, Set.image_subtype_val_uIoc, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, CategoryTheory.TransfiniteCompositionOfShape.iic_F, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, SSet.hornββ.desc.multicofork_Ο_zero_assoc, Ordinal.ord_cof_eq, hahnEmbedding_isOrderedModule_rat, SSet.hornββ.desc.multicofork_Ο_three_assoc, SSet.hornββ.desc.multicofork_Ο_zero, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, HahnEmbedding.Partial.eval_lt, SSet.hornββ.desc.multicofork_Ο_three, SSet.hornββ.desc.multicofork_pt, Ordinal.type_Iio_lt, HahnEmbedding.Partial.sSupFun_strictMono, unitInterval.volume_uIoc, SSet.hornββ.desc.multicofork_Ο_zero, SSet.hornββ.desc.multicofork_Ο_three_assoc, SSet.hornββ.desc.multicofork_Ο_one_assoc, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, SSet.hornββ.desc.multicofork_Ο_three, hahnEmbedding_isOrderedAddMonoid, Set.image_subtype_val_uIcc, hahnEmbedding_isOrderedModule, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|
partialOrder π | CompOp | 106 mathmath: HahnEmbedding.Seed.baseEmbedding_pos, HahnEmbedding.IsPartial.baseEmbedding_le, disjoint_subtype_iff, Nonneg.isStrictOrderedRing, Set.Iic.isCompactElement, Subsemiring.toIsOrderedRing, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, Module.End.invtSubmodule.disjoint_mk_iff, Nonneg.isOrderedRing, Subring.toIsOrderedRing, HahnEmbedding.Partial.baseEmbedding_le_sSupFun, CategoryTheory.TransfiniteCompositionOfShape.iic_isoBot, HahnEmbedding.Partial.archimedeanClassMk_eq_iff, HahnEmbedding.Partial.truncLT_mem_range_extendFun, HahnEmbedding.Seed.baseEmbedding_strictMono, isAtomic_iff_forall_isAtomic_Iic, Set.Icc.disjoint_iff, Set.Iic.isCompl_inf_inf_of_isCompl_of_le, Nonneg.segment_eq_uIcc, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Set.Icc.codisjoint_iff, HahnEmbedding.Partial.orderTop_eq_iff, Subsemiring.toIsStrictOrderedRing, HahnEmbedding.Partial.lt_extend, HahnEmbedding.Partial.coeff_eq_of_mem, HahnEmbedding.Partial.extendFun_strictMono, CategoryTheory.TransfiniteCompositionOfShape.iic_isColimit, HahnEmbedding.IsPartial.strictMono, CompleteLattice.Iic_coatomic_of_compact_element, Module.End.invtSubmodule.isCompl_iff, Valuation.nonempty_rankOne_iff_mulArchimedean, HahnEmbedding.Partial.exists_sub_mem_ball, HahnEmbedding.IsPartial.truncLT_mem_range, Subring.toIsStrictOrderedRing, Complementeds.codisjoint_coe, IsAtomic.Set.Iic.isAtomic, isCoatomic_iff_forall_isCoatomic_Ici, HahnEmbedding.Partial.truncLT_mem_range_sSupFun, CategoryTheory.Functor.IsWellOrderContinuous.nonempty_isColimit, CompleteSublattice.codisjoint_iff, Set.Iic.disjoint_iff, CategoryTheory.SmallObject.coconeOfLE_pt, CompleteSublattice.isCompl_iff, HahnEmbedding.Partial.eval_smul, Nonneg.instArchimedean, HahnEmbedding.Partial.le_sSupFun, Set.Ici.disjoint_iff, Set.Ici.codisjoint_iff, Valued.integer.mulArchimedean_mrange_of_isCompact_integer, HahnEmbedding.Seed.coeff_baseEmbedding, Subalgebra.toIsStrictOrderedRing, SubsemiringClass.toIsOrderedRing, IsCoatomic.Set.Ici.isCoatomic, CategoryTheory.TransfiniteCompositionOfShape.iic_F, Set.Icc.isCompl_iff, CategoryTheory.SmallObject.restrictionLE_map, CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci, HahnEmbedding.Partial.coeff_eq_zero_of_mem, HahnEmbedding.Partial.orderTop_eq_finiteArchimedeanClassMk, Module.End.invtSubmodule.isCompl_mk_iff, AddSubmonoidClass.instAddArchimedean, hahnEmbedding_isOrderedModule_rat, Module.End.invtSubmodule.codisjoint_iff, HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding, HahnEmbedding.Partial.mem_domain, Set.Iic.codisjoint_iff, HahnEmbedding.Seed.mem_domain_baseEmbedding, CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app, codisjoint_subtype_iff, HahnEmbedding.Partial.eval_lt, SubmonoidClass.instMulArchimedean, HahnEmbedding.ArchimedeanStrata.archimedean_stratum, Subalgebra.toIsOrderedRing, Nonneg.nat_ceil_coe, Set.Iic.isCompl_iff, Complementeds.isCompl_coe, Module.End.isSemisimple_iff', Set.Ici.isCompl_iff, HahnEmbedding.Partial.archimedeanClassMk_le_of_eval_eq, HahnEmbedding.Partial.baseEmbedding_le_extendFun, Nonneg.Icc_subset_segment, CategoryTheory.SmallObject.restrictionLT_map, HahnEmbedding.Partial.eval_zero, HahnEmbedding.Partial.eval_eq_truncLT, CompleteSublattice.disjoint_iff, Nonneg.nat_floor_coe, HahnEmbedding.Partial.evalCoeff_eq, HahnEmbedding.Partial.sSupFun_strictMono, SubsemiringClass.toIsStrictOrderedRing, CategoryTheory.SmallObject.coconeOfLE_ΞΉ_app, Nonneg.instMulArchimedean, HahnEmbedding.Partial.exists_domain_eq_top, HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun, Set.Ioc.codisjoint_iff, Module.End.invtSubmodule.codisjoint_mk_iff, HahnEmbedding.Partial.exists_isMax, HahnEmbedding.Partial.apply_of_mem_stratum, Set.Ico.disjoint_iff, Module.End.invtSubmodule.disjoint_iff, HahnEmbedding.Seed.domain_baseEmbedding, Subfield.toIsStrictOrderedRing, Complementeds.disjoint_coe, hahnEmbedding_isOrderedAddMonoid, Nonneg.segment_eq_Icc, hahnEmbedding_isOrderedModule, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|
preorder π | CompOp | 414 mathmath: Valuation.mem_nhds_zero_iff, AddSubmonoid.toIsOrderedCancelAddMonoid, Valued.isOpen_closedball, Submodule.FG.rTensor.directedSystem, Set.image_subtype_val_Ici_Ici, Subring.orderedSubtype_coe, WithVal.valueGroupOrderIsoβ_symm_apply, Valuation.isClopen_closedBall, Set.image_subtype_val_Ioi_Ioi, unitInterval.volume_Ioo, unitInterval.volume_Iic, Submodule.toIsOrderedAddMonoid, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map_le_succ, Set.preimage_subtype_val_Ioi, Filter.atTop_Ici_eq, SupConvergenceClass.tendsto_coe_atTop_isLUB, MeasureTheory.Lp.instIsOrderedAddMonoid, unitInterval.strictAnti_symm, comap_coe_Ioi_nhdsGT, ProbabilityTheory.unitInterval.cdf_eq_real, WithBot.subtypeOrderIso_symm_apply, exists_monotone_Icc_subset_open_cover_Icc, Ordinal.cof_Iio, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, MeasureTheory.Measure.toSphere_apply_aux, WithVal.valueGroupOrderIsoβ_restrict, Path.range_subpath_of_ge, Set.Iic.succ_eq_of_not_isMax, SubmonoidClass.toIsOrderedMonoid, Finset.subtype_Ioc_eq, HasCardinalLT.Set.functor_obj, Set.image_subtype_val_Iio_subset, MonoidWithZeroHom.ValueGroupβ.monoidWithZeroHom_strictMono, WithVal.valueGroupOrderIsoβ_apply, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ, Set.strictMonoOn_projIic, unitInterval.volume_Ico, CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map, Submodule.FG.lTensor.directedSystem, covBy_iff_coatom_Iic, Finset.subtype_Ico_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, comap_coe_nhdsLT_of_Ioo_subset, unitInterval.sigmoid_strictMono, ringKrullDim_quotient, Submonoid.topOrderMonoidIso_symm_apply_coe, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_obj, Filter.tendsto_Iic_atBot, idealFactorsFunOfQuotHom_comp, Set.image_subtype_val_Ico_subset, HasCardinalLT.Set.cocone_pt, HahnEmbedding.Seed.baseEmbedding_strictMono, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_assoc, Valued.isClopen_ball, ValuativeRel.ValueGroupWithZero.embed_strictMono, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, Set.monotone_projIic, Set.Ici.isAtom_iff, CategoryTheory.SmallObject.SuccStruct.arrowMap_refl, Tuple.monotone_proj, Valuation.hasBasis_nhds_zero, Set.antitoneOn_iff_antitone, ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrictβ, Valuation.restrict_le_iff, Valuation.IsRankOneDiscrete.valueGroupβ_equiv_withZeroMulInt_strictMono, OrderHom.Subtype.val_coe, HahnEmbedding.Partial.toOrderAddMonoidHom_apply, Matroid.isClosed_iff_isFlat, Valued.is_topological_valuation, CategoryTheory.TransfiniteCompositionOfShape.ici_F, HahnEmbedding.Seed.strictMono_coeff, IsValuativeTopology.isOpen_ball, Set.image_subtype_val_Ico_Iio, SSet.stdSimplex.face_eq_ofSimplex, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc, Set.preimage_subtype_val_Iic, ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso, FiniteMulArchimedeanClass.withTopOrderIso_apply_coe, map_coe_Ioo_atBot, Valuation.restrict_lt_iff_lt_embedding, Set.image_subtype_val_Ioc_Ici, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, HahnEmbedding.Partial.extendFun_strictMono, tendsto_comp_coe_Iio_atTop, CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_inv_app, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq, Filter.atTop_Ioi_eq, Finset.subtype_Iio_eq, Filter.tendsto_comp_val_Iic_atBot, tendsto_Ioi_atBot, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality, Valuation.restrict_le_iff_le_embedding, unitInterval.volume_Ici, Matroid.closure_eq_subtypeClosure, HahnEmbedding.IsPartial.strictMono, MulEquiv.strictMono_subsemigroupCongr, Irrational.instOrderTopologySubtypeReal, Set.image_subtype_val_Iio_Iio, Filter.map_val_Ici_atTop, FiniteArchimedeanClass.liftOrderHom_mk, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_hom_app, Valued.hasBasis_nhds_zero, Set.image_subtype_val_Ioo_Ioi, Set.image_subtype_val_Ici_Iio, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.w, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_map, Set.monotoneOn_iff_monotone, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality, WithVal.strictMono_valueGroupOrderIsoβ, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot, WithVal.strictMono_valueGroupOrderIsoβ_symm, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.tgt, Set.image_subtype_val_Ioi_subset, Ordinal.IsFundamentalSeq.strictMono, AddSubmonoidClass.toIsOrderedCancelAddMonoid, Submodule.FG.lTensor.directLimit_apply', instIsStronglyCoatomicElemOfOrdConnected, Valuation.RankOne.strictMono, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality_assoc, unitInterval.volume_Icc, unitInterval.range_sigmoid, Submodule.FG.rTensor.directLimit_apply, Set.image_subtype_val_Ico, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj, ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk, Valued.isClosed_ball, Valuation.restrict_lt_one_iff, FiniteMulArchimedeanClass.withTopOrderIso_symm_apply, PNat.equivNonZeroDivisorsNat_symm_apply_coe, FiniteMulArchimedeanClass.liftOrderHom_mk, WithTop.subtypeOrderIso_symm_apply, IsValuativeTopology.isClosed_closedBall, coe_pred_of_mem, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, Finset.map_subtype_embedding_Ioi, covBy_iff_atom_Ici, CategoryTheory.SmallObject.coconeOfLE_pt, Valuation.cauchy_iff, StrictMono.codRestrict, Subsemigroup.strictMono_topEquiv, Order.coheight_eq_krullDim_Ici, Filter.map_val_atTop_of_Ici_subset, Order.cof_Iio, mono_coe, ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed, Filter.atBot_Iic_eq, AddSubsemigroup.strictMono_topEquiv, IsAtom.Iic, exists_monotone_Icc_subset_open_cover_unitInterval_prod_self, AddSubgroup.toIsOrderedAddMonoid, Set.strictMonoOn_projIcc, Order.height_eq_krullDim_Iic, Filter.tendsto_Ioi_atTop, coe_succ_of_mem, AddEquiv.strictMono_subsemigroupCongr, Valued.cauchy_iff, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ, CategoryTheory.TransfiniteCompositionOfShape.ici_isoBot, comap_coe_nhdsLT_eq_atTop_iff, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq, CategoryTheory.SmallObject.SuccStruct.restrictionLTOfCoconeIso_hom_app, Finset.map_subtype_embedding_Ioc, Filter.tendsto_Iio_atBot, CategoryTheory.SmallObject.SuccStruct.arrowΞΉ_def, Set.OrdConnected.isSuccArchimedean, Set.image_subtype_val_Iic_Iic, CategoryTheory.SmallObject.restrictionLE_map, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top, Positive.isOrderedMonoid, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans_assoc, map_coe_Ioo_atTop, map_coe_atBot_of_Ioo_subset, Valuation.restrict_pos_iff, IsValuativeTopology.isClopen_ball, map_coe_Ioi_atBot, Set.OrdConnected.isStronglyAtomic, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_inv_app, Set.image_subtype_val_Ico_Iic, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, Equiv.image_strictAnti, Set.preimage_subtype_val_Ico, Set.image_subtype_val_Ioc_Iio, Valuation.IsEquiv.orderMonoidIso_trans, WithVal.strictMono_valueGroupEquiv_symm, Set.preimage_subtype_val_Ioo, CategoryTheory.TransfiniteCompositionOfShape.ici_isColimit, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, Valuation.isClosed_closedBall, Set.Ici.coe_pred_of_not_isMin, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt, Set.OrdConnected.restrict, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_refl, Set.image_subtype_val_Iic_Iio, tendsto_comp_coe_Ioo_atBot, Filter.tendsto_comp_val_Iio_atBot, IsValuativeTopology.isOpen_closedBall, StrictMonoOn.strictMono, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top, CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci, Set.strictMonoOn_projIci, Equiv.Set.Equiv.strictMono_setCongr, CategoryTheory.Limits.preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape, Monotone.codRestrict, Set.image_subtype_val_Ioc_Ioi, Set.image_subtype_val_Ioo, Set.image_subtype_val_Iio_Iic, unitInterval.subtype_Ici_eq_Icc, Finset.map_subtype_embedding_Iio, CategoryTheory.SmallObject.SuccStruct.Iteration.subsingleton.MapEq.src, unitInterval.subtype_Iio_eq_Ico, Valuation.isClopen_ball, Submonoid.toIsOrderedMonoid, SubmonoidClass.toIsOrderedCancelMonoid, Set.image_subtype_val_Ioo_Ici, MonotoneOn.monotone, HasCardinalLT.Set.cocone_ΞΉ_app, hahnEmbedding_isOrderedModule_rat, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq, Subgroup.toIsOrderedMonoid, Submodule.toIsOrderedCancelAddMonoid, Valued.isOpen_closedBall, Valuation.hasBasis_nhds, unitInterval.volume_Ioc, Set.monotone_projIcc, AddSubmonoidClass.toIsOrderedAddMonoid, Positive.isOrderedCancelMonoid, Valued.mem_nhds_zero, Flag.grade_coe, PNat.equivNonZeroDivisorsNat_apply_coe, Nonneg.instIsOrderedModule, Valued.isOpen_ball, Finset.map_subtype_embedding_Ici, Set.Iic.coe_succ_of_not_isMax, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, Set.image_subtype_val_Iic_subset, Valued.mem_nhds, FiniteArchimedeanClass.withTopOrderIso_symm_apply, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_limit, Submodule.FG.directedSystem, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map, strictMono_restrict, HasCardinalLT.Set.functor_map_coe, Valuation.isOpen_ball, Valued.integer.locallyFiniteOrder_units_mrange_of_isCompact_integer, tendsto_comp_coe_Ioo_atTop, WithBot.subtypeOrderIso_apply_coe, Equiv.image_strictMono, Set.image_subtype_val_Icc_Ici, StrictMonoOn.restrict, instIsStronglyAtomicElemOfOrdConnected, AddSubmonoid.toIsOrderedAddMonoid, IsValuativeTopology.isClosed_ball, Filter.map_val_Ioi_atTop, Submodule.FG.lTensor.directLimit_apply, Module.fgSystem.equiv_comp_of, WithVal.valueGroupOrderIsoβ_symm_restrict, Filter.tendsto_comp_val_Ici_atTop, tendsto_Ioo_atBot, Set.image_subtype_val_Ioi_Ici, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_succ_eq, Set.Ici.pred_eq_of_not_isMin, Set.image_subtype_val_Ici_Iic, ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq, Set.image_subtype_val_Ioc, Tuple.eq_sort_iff', FiniteMulArchimedeanClass.ballSubgroup_strictAnti, Valuation.hasBasis_uniformity, idealFactorsFunOfQuotHom_id, Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support, Set.preimage_subtype_val_Ioc, HasCardinalLT.Set.instIsCardinalFiltered, Nonneg.isOrderedAddMonoid, Valuation.Integers.wellFounded_gt_on_v_iff_discrete_mrange, Set.Icc.monotone_addNSMul, CategoryTheory.SmallObject.SuccStruct.Iteration.congr_map, StrictAntiOn.strictAnti, instOrderClosedTopology, Valuation.restrict_le_one_iff, Valuation.isClosed_ball, CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc, MeasureTheory.Lp.instOrderClosedTopologySubtypeAEEqFunMemAddSubgroupOfClosedIciTopology, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor_obj, Valuation.IsEquiv.orderMonoidIso_eq_refl, unitInterval.sigmoid_monotone, Equiv.image_antitone, Submonoid.toIsOrderedCancelMonoid, WithTop.subtypeOrderIso_apply_coe, Monotone.restrict, FiniteArchimedeanClass.ballAddSubgroup_strictAnti, CategoryTheory.Functor.WellOrderInductionData.map_lift, Valued.hasBasis_uniformity, Set.image_subtype_val_Icc_Iio, ValuativeRel.valuation_lt_symm_orderMonoidIso, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, Set.image_subtype_val_Ioc_subset, Matroid.isFlat_iff_isClosed, Set.image_subtype_val_Iio_Ioi, Set.image_subtype_val_Icc_Ioi, Filter.atBot_Iio_eq, Set.OrdConnected.isPredArchimedean, tendsto_Ioo_atTop, Set.image_subtype_val_Ioo_subset, CategoryTheory.SmallObject.restrictionLT_obj, CategoryTheory.Limits.HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit, exists_monotone_Icc_subset_open_cover_unitInterval, Valuation.restrict_lt_iff, CategoryTheory.SmallObject.restrictionLE_obj, Nonneg.Icc_subset_segment, idealFactorsFunOfQuotHom_coe_coe, Valued.isClosed_closedBall, Valuation.isOpen_closedBall, MeasureTheory.Measure.volumeIoiPow_apply_Iio, Finset.map_subtype_embedding_Ico, FiniteArchimedeanClass.ball_strictAnti, CategoryTheory.SmallObject.restrictionLT_map, CategoryTheory.SmallObject.SuccStruct.ofCocone_map, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj, Finset.subtype_Iic_eq, Filter.map_val_Iio_atBot, Set.image_subtype_val_Ici_subset, unitInterval.univ_eq_Icc, comap_coe_Iio_nhdsLT, Finset.subtype_Ici_eq, AntitoneOn.monotone, unitInterval.subtype_Iic_eq_Icc, Set.image_subtype_val_Ioi_Iic, ValuativeRel.restrict_lt_orderMonoidIso, comap_coe_nhdsGT_of_Ioo_subset, Set.Ici.subtype_functor_final, Set.OrdConnected.isStronglyCoatomic, HahnEmbedding.Partial.sSupFun_strictMono, Filter.tendsto_comp_val_Ioi_atTop, CategoryTheory.Limits.PreservesWellOrderContinuousOfShape.preservesColimitsOfShape, CategoryTheory.SmallObject.coconeOfLE_ΞΉ_app, Set.image_subtype_val_Iic_Ici, Set.image_subtype_val_Iic_Ioi, HasCardinalLT.Set.instIsFilteredOfFactIsRegular, CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit, Path.range_subpath_of_le, Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId, Finset.map_subtype_embedding_Ioo, Valuation.IsEquiv.orderMonoidIso_spec, Submonoid.topOrderMonoidIso_apply, unitInterval.subtype_Ioi_eq_Ioc, Set.image_subtype_val_Iio_Ici, Valued.isClopen_closedBall, WithVal.strictMono_valueGroupEquiv, InfConvergenceClass.tendsto_coe_atBot_isGLB, MonoidWithZeroHom.ValueGroupβ.instIsOrderedMonoid, closureOperator_gi_self, IsCoatom.Ici, Flag.coe_wcovBy_coe, Set.image_subtype_val_Ioi_Iio, Filter.tendsto_Ici_atTop, map_coe_atTop_of_Ioo_subset, Set.image_subtype_val_Ico_Ici, comap_coe_nhdsGT_eq_atBot_iff, Valuation.RankLeOne.strictMono', Finset.subtype_Ioo_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.prop_map_succ, Monotone.rangeFactorization, Equiv.image_monotone, CategoryTheory.TransfiniteCompositionOfShape.ici_incl, Valuation.exists_setOf_restrict_le_iff, Submodule.FG.rTensor.directLimit_apply', ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono, Set.Iic.isCoatom_iff, HasCardinalLT.Set.isFiltered_of_aleph0_le, Finset.subtype_Icc_eq, Set.image_subtype_val_Ioc_Iic, Set.image_subtype_val_Icc_subset, orderTopology_of_ordConnected, Set.preimage_subtype_val_Icc, Set.image_subtype_val_Ici_Ioi, Set.strictAntiOn_iff_strictAnti, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj_trans, MonoidWithZeroHom.ValueGroupβ.embedding_strictMono, Set.image_subtype_val_Icc_Iic, FiniteArchimedeanClass.withTopOrderIso_apply_coe, Finset.map_subtype_embedding_Iic, Set.preimage_subtype_val_Iio, Set.image_subtype_val_Icc, IsValuativeTopology.isClopen_closedBall, Valuation.mem_nhds_iff, tendsto_comp_coe_Ioi_atBot, Finset.subtype_Ioi_eq, Set.image_subtype_val_Ioo_Iio, Filter.map_val_Iic_atBot, Set.monotone_projIci, Finset.map_subtype_embedding_Icc, Set.image_subtype_val_Ioo_Iic, Set.preimage_subtype_val_Ici, strictMono_coe, Valuation.is_topological_valuation, comap_coe_Ioo_nhdsGT, Valuation.IsEquiv.orderMonoidIso_symm, hahnEmbedding_isOrderedAddMonoid, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj, unitInterval.volume_Iio, Nonneg.segment_eq_Icc, map_coe_Iio_atTop, Nonneg.isOrderedCancelAddMonoid, tendsto_Iio_atTop, Nonneg.instIsStrictOrderedModule, hahnEmbedding_isOrderedModule, CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit, Set.strictMonoOn_iff_strictMono, Set.image_subtype_val_Ico_Ioi, unitInterval.volume_Ioi, comap_coe_Ioo_nhdsLT, HahnEmbedding.Partial.toOrderAddMonoidHom_injective
|