| Metric | Count |
|---|
DefinitionstoOrderIso, dual, gtEmbedding, ltEmbedding, ofIsEmpty, ofMapLEIff, ofStrictMono, subtype, toOrderHom, OrderHom, val, apply, coeFnHom, comp, compโ, const, copy, curry, diag, dual, dualIso, fst, id, instDecidableEqOfForall, instFunLike, instInhabited, instPartialOrder, instPreorder, onDiag, pi, piIso, prod, prodIso, prodMap, prodโ, snd, toFun, uliftLeftMap, uliftMap, uliftRightMap, unique, OrderHomClass, instCoeTCOrderHom, toOrderHom, arrowCongr, conj, dual, dualDual, funUnique, instEquivLike, ofCmpEqCmp, ofHomInv, ofIsEmpty, ofRelIsoLT, ofUnique, prodAssoc, prodComm, refl, toOrderEmbedding, toRelIsoGT, toRelIsoLT, trans, OrderIsoClass, toOrderIso, evalOrderHom, orderEmbeddingOfLTEmbedding, toOrderHom, orderIsoOfRightInverse, orderEmbedding, orderIso, instCoeTCOrderIsoOfOrderIsoClass, instFunLikeOrderEmbedding, instFunLikeOrderIso, ยซterm_โo_ยป, ยซterm_โชo_ยป, ยซterm_โo_ยป | 76 |
Theoremsmap_orderIso, of_orderEmbedding, map_orderIso, of_orderEmbedding, coe_toOrderIso, toOrderIso_toEquiv, of_orderEmbedding, acc, coe_ofIsEmpty, coe_ofMapLEIff, coe_ofStrictMono, coe_subtype, eq_iff_eq, gtEmbedding_apply, isWellOrder, le_iff_le, le_map_sup, ltEmbedding_apply, lt_iff_lt, map_inf_le, monotone, ofIsEmpty_apply, strictMono, subtype_apply, subtype_injective, toOrderHom_coe, wellFounded, wellFoundedGT, wellFoundedLT, val_coe, apply_coe, apply_mono, canLift, coeFnHom_coe, coe_copy, coe_eq, coe_le_coe, coe_mk, comp_coe, comp_const, comp_id, comp_mono, comp_prod_comp_same, compโ_coe_coe_coe, const_coe_coe, const_comp, copy_eq, curry_apply, curry_symm_apply, diag_coe, dual_apply_coe, dual_comp, dual_id, dual_symm_apply_coe, ext, ext_iff, fst_coe, fst_comp_prod, fst_prod_snd, id_coe, id_comp, instOrderHomClass, le_def, mk_comp_mk, mk_le_mk, mono, monotone, monotone', onDiag_coe, orderHom_eq_id, piIso_apply, piIso_symm_apply, pi_coe, prodIso_apply, prodIso_symm_apply, prodMap_coe, prod_coe, prod_mono, prodโ_coe_coe_coe, snd_coe, snd_comp_prod, symm_dual_comp, symm_dual_id, toFun_eq_coe, uliftLeftMap_coe, uliftLeftMap_uliftRightMap_eq, uliftMap_coe_down, uliftRightMap_coe_down, uliftRightMap_uliftLeftMap_eq, coe_coe, mono, monotone, toOrderHomClassOrderDual, apply_eq_iff_eq, apply_eq_iff_eq_symm_apply, apply_symm_apply, arrowCongr_apply, arrowCongr_symm_apply, bijective, coe_dualDual, coe_dualDual_symm, coe_prodComm, coe_refl, coe_symm_toEquiv, coe_symm_toRelIsoGT, coe_symm_toRelIsoLT, coe_toEquiv, coe_toOrderEmbedding, coe_toRelIsoGT, coe_toRelIsoLT, coe_trans, complementedLattice, complementedLattice_iff, conj_apply, conj_symm_apply, dualDual_apply, dualDual_symm_apply, dual_apply, dual_symm_apply, ext, ext_iff, funUnique_apply, funUnique_symm_apply, funUnique_toEquiv, injective, instOrderIsoClass, isCompl, isCompl_iff, isMax_apply, isMin_apply, le_iff_le, le_symm_apply, lt_iff_lt, lt_symm_apply, map_bot, map_bot', map_inf, map_sup, map_top, map_top', monotone, ofHomInv_apply, ofHomInv_symm_apply, ofRelIsoLT_apply, ofRelIsoLT_symm, ofRelIsoLT_toRelIsoLT, ofUnique_apply, ofUnique_symm_apply, prodAssoc_apply, prodAssoc_symm_apply, prodComm_symm, refl_apply, refl_toEquiv, refl_trans, self_trans_symm, strictMono, surjective, symm_apply_apply, symm_apply_eq, symm_apply_le, symm_apply_lt, symm_bijective, symm_dual, symm_injective, symm_mk, symm_refl, symm_symm, symm_trans, symm_trans_apply, symm_trans_self, toEquiv_symm, toFun_eq_coe, toRelIsoGT_apply, toRelIsoGT_symm, toRelIsoLT_apply, toRelIsoLT_ofRelIsoLT, toRelIsoLT_symm, trans_apply, trans_refl, map_le_map_iff, toOrderHomClass, toOrderIsoClassOrderDual, evalOrderHom_coe, orderEmbeddingOfLTEmbedding_apply, toOrderHom_injective, toOrderHom_coe, denselyOrdered_range, orderIsoOfRightInverse_apply, orderIsoOfRightInverse_symm_apply, orderEmbedding_apply_coe, orderIso_apply, orderIso_symm_apply_down, codisjoint_map_orderIso_iff, denselyOrdered_iff_of_orderIsoClass, denselyOrdered_iff_of_strictAnti, disjoint_map_orderIso_iff, le_map_inv_iff, lt_map_inv_iff, map_inv_le_iff, map_inv_le_map_inv_iff, map_inv_lt_iff, map_inv_lt_map_inv_iff, map_lt_map_iff | 203 |
| Total | 279 |
| Name | Category | Theorems |
|---|
apply ๐ | CompOp | 4 mathmath: OmegaCompletePartialOrder.ContinuousHom.ฯSup_apply, OmegaCompletePartialOrder.OrderHom.ฯSup_coe, apply_coe, OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ฯSup_coe
|
coeFnHom ๐ | CompOp | 1 mathmath: coeFnHom_coe
|
comp ๐ | CompOp | 48 mathmath: OrderIso.arrowCongr_apply, OrderAddMonoidHom.coe_comp_orderHom, Topology.WithLowerSet.map_comp, idealFactorsFunOfQuotHom_comp, prodIso_apply, SSet.stdSimplex.face_eq_ofSimplex, SSet.prodStdSimplex.objEquiv_naturality, comp_const, SimplexCategory.II.map'_map', FinPartOrd.hom_hom_comp, NonemptyFinLinOrd.hom_comp, OrderIso.conj_apply, OrderIso.arrowCongr_symm_apply, comp_prod_comp_same, snd_comp_prod, lfp_lfp, gfp_gfp, dual_comp, Preord.hom_comp, LinOrd.ofHom_comp, id_comp, mk_comp_mk, comp_coe, fst_comp_prod, symm_dual_comp, BoundedOrderHom.coe_comp_orderHom, NonemptyFinLinOrd.hom_hom_comp, Preord.ofHom_comp, LinOrd.hom_comp, comp_mono, SimplexCategory.comp_toOrderHom, Topology.WithUpperSet.map_comp, OrderMonoidHom.coe_comp_orderHom, Pi.uncurry_curry_ฯScottContinuous, piIso_apply, comp_id, Interval.map_map, PartOrd.hom_comp, Specialization.map_comp, FinPartOrd.hom_comp, PartOrd.ofHom_comp, map_lfp_comp, NonemptyInterval.map_map, CategoryTheory.SimplicialThickening.functor_comp, map_gfp_comp, const_comp, OmegaCompletePartialOrder.Chain.map_comp, PseudoEpimorphism.coe_comp_orderHom
|
compโ ๐ | CompOp | 1 mathmath: compโ_coe_coe_coe
|
const ๐ | CompOp | 7 mathmath: top_def, gfp_const_inf_le, comp_const, bot_def, SSet.stdSimplex.const_down_toOrderHom, const_coe_coe, const_comp
|
copy ๐ | CompOp | 2 mathmath: coe_copy, copy_eq
|
curry ๐ | CompOp | 2 mathmath: curry_apply, curry_symm_apply
|
diag ๐ | CompOp | 1 mathmath: diag_coe
|
dual ๐ | CompOp | 15 mathmath: NonemptyInterval.dual_map, dual_id, LinOrd.dual_map, BoundedOrderHom.dual_apply_toOrderHom, PartOrd.dual_map, symm_dual_id, FinPartOrd.dual_map, dual_comp, NonemptyFinLinOrd.dual_map, Preord.dual_map, BoundedOrderHom.dual_symm_apply_toOrderHom, symm_dual_comp, dual_apply_coe, dual_symm_apply_coe, Interval.dual_map
|
dualIso ๐ | CompOp | โ |
fst ๐ | CompOp | 6 mathmath: prodIso_apply, fst_prod_snd, fst_comp_prod, fst_coe, Prod.ฯSupImpl_fst, Prod.ฯSup_fst
|
id ๐ | CompOp | 28 mathmath: OmegaCompletePartialOrder.Chain.map_id, Preord.ofHom_id, dual_id, LinOrd.hom_id, id_coe, orderHom_eq_id, SSet.stdSimplex.map_id, LinOrd.ofHom_id, symm_dual_id, Preord.hom_id, SimplexCategory.id_toOrderHom, NonemptyFinLinOrd.hom_hom_id, PartOrd.ofHom_id, id_comp, Topology.WithLowerSet.map_id, fst_prod_snd, FinPartOrd.hom_id, idealFactorsFunOfQuotHom_id, SimplexCategory.concreteCategoryHom_id, SimplexCategory.II.map'_id, Specialization.map_id, comp_id, CategoryTheory.SimplicialThickening.functor_id, FinPartOrd.hom_hom_id, PartOrd.hom_id, PseudoEpimorphism.coe_id_orderHom, NonemptyFinLinOrd.hom_id, Topology.WithUpperSet.map_id
|
instDecidableEqOfForall ๐ | CompOp | โ |
instFunLike ๐ | CompOp | 560 mathmath: Behrend.roth_lower_bound, partialSups_apply, HurwitzZeta.hasSum_int_hurwitzZetaOdd, sign_intCast, hasSum_mellin_pi_mul_sq', rothNumberNat_spec, LinearMap.iterateRange_succ, SSet.stdSimplex.coe_triangle_down_toOrderHom, SimplexCategory.eq_const_of_zero, sign_mul_self, NonemptyInterval.map_pure, partialSups_const_add, LinOrd.ofHom_apply, partialSups_succ', deriv_abs, Affine.Simplex.sign_excenterWeights_singleton_pos, le_map_sup_fixedPoints, SSet.ofSimplex_le_skeleton, Part.Fix.exists_fix_le_approx, OrdinalApprox.gfp_mem_range_gfpApprox, signHom_apply, WellFoundedGT.monotone_chain_condition, ciSup_partialSups_eq', CategoryTheory.Functor.toOrderHom_coe, Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, Fin.orderHom_injective_iff, SimplexCategory.const_comp, Module.End.independent_genEigenspace, le_addRothNumber_product, Behrend.roth_lower_bound_explicit, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, Filter.Tendsto.partialSups_apply, OrderAddMonoidHom.coe_orderHom, id_coe, rothNumberNat_le, partialSups_eq_sup'_range, MulArchimedeanClass.orderHom_injective, lfp_le_gfp, Part.toUnitMono_coe, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, IsArtinian.eventuallyConst_of_isArtinian, monotone, TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, EReal.sign_eq_and_abs_eq_iff_eq, WellFoundedGT.iSup_eq_monotonicSequenceLimit, OmegaCompletePartialOrder.OrderHom.ฯSup_coe, Module.End.genEigenspace_directed, SSet.prodStdSimplex.orderHomOfSimplex_coe, sign_nonneg_iff, antisymmetrization_apply, biUnion_range_succ_disjointed, map_lfp, Module.End.maxGenEigenspace_eq, SemilatInfCat_dual_comp_forget_to_partOrd, BoxIntegral.Box.Ioo_subset_coe, partialSups_add_one', top_def, Preord.coe_id, Behrend.bound_aux', gfp_const_inf_le, Affine.Simplex.sign_touchpointWeights_empty, TwoSidedIdeal.bot_asIdeal, Preord.ext_iff, coe_antisymmetrization, Part.Fix.approx_mem_approxChain, SSet.prodStdSimplex.objEquiv_apply_fst, ClosureOperator.conjBy_apply, iSup_partialSups_eq, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, mulRothNumber_map_mul_left, Prod.Lex.toLexOrderHom_coe, Preord.inv_hom_apply, Module.End.mapsTo_genEigenspace_of_comm, partialSups_const_mul, snd_coe, iInf_apply, Preord.hom_inv_apply, Part.Fix.approx_le_fix, HasStrictFDerivAt.abs, Ideal.toTwoSided_asIdeal, NonemptyFinLinOrd.epi_iff_surjective, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, LinOrd.hom_inv_apply, SSet.iSup_skeleton, partialSups_add_one, Finset.insertNone_eraseNone, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkOfSucc_homToOrderHom_one, sSup_apply, Subtype.val_coe, SimplexCategory.Hom.mk_toOrderHom_apply, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, coe_le_coe, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, PartOrd.coe_id, Preord.ofHom_apply, hasDerivWithinAt_abs, SSet.skeleton_le_skeletonOfMono, SSet.prodStdSimplex.objEquiv_ฮด_apply, Finset.card_eraseNone_le, EReal.abs_mul_sign, Finset.eraseNone_union, mulRothNumber_spec, Finset.eraseNone_none, LinOrd.inv_hom_apply, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, Submodule.inf_genEigenspace, withBotMap_coe, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, ThreeAPFree.addRothNumber_eq, sign_zero, disjoint_partialSups_right, comp_const, SimplexCategory.toTop_map, ArchimedeanClass.orderHom_zero, NormedSpace.normalize_smul, sign_mul_abs, sign_eq_of_affineCombination_mem_affineSpan_single_lineMap, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, MulArchimedeanClass.liftOrderHom_mk, BoxIntegral.Box.iUnion_Ioo_of_tendsto, prodMap_coe, ContinuousWithinAt.partialSups_apply, addRothNumber_union_le, Interval.subset_coe_map, sign_pos, le_partialSups_of_le, OmegaCompletePartialOrder.Chain.mem_map, comp_partialSups, Finset.card_eraseNone_of_not_mem, SimplexCategory.toTopโ_map, CircleDeg1Lift.coe_mk, SSet.prodStdSimplex.objEquiv_apply_snd, LinearMap.finrank_genEigenspace_le, partialSups_eq_sup_range, SimplexCategory.congr_toOrderHom_apply, HasFDerivAt.abs, HasFDerivWithinAt.abs, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, Module.End.iSup_genEigenspace_eq, le_def, Finset.card_eraseNone_of_mem, LinOrd.id_apply, Module.End.genEigenspace_inf_le_add, FiniteArchimedeanClass.liftOrderHom_mk, partialSups_monotone, Module.End.eigenspace_le_genEigenspace, rothNumberNat_zero, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, BoxIntegral.Box.Ioo_ae_eq_Icc, FinBoolAlg.forgetToFinPartOrdFaithful, Fin.addRothNumber_eq_rothNumberNat, IsMulFreimanHom.mulRothNumber_mono, SSet.horn_obj, disjointed_add_one, SSet.skeleton_obj_eq_top, partialSups_mul_const, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, Preord.id_apply, OrderMonoidIso.coe_orderIso, EReal.sign_mul, isLeast_lfp, ContinuousOrderHom.coe_toOrderHom, bddOrd_dual_comp_forget_to_partOrd, partialSups_succ, EReal.sign_coe, SSet.stdSimplex.face_obj, Affine.Simplex.sign_excenterWeights_singleton_neg, pi_coe, partialSups_le, Finset.image_some_eraseNone, ThreeGPFree.le_mulRothNumber, SSet.Truncated.spine_map_vertex, OrdinalApprox.lfpApprox_ord_eq_lfp, classifyingSpaceUniversalCover_map, gfp_le, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, addRothNumber_spec, eventually_nhdsWithin_sign_eq_of_deriv_neg, OmegaCompletePartialOrder.ฯScottContinuous_iff_map_ฯSup_of_orderHom, SSet.mem_skeleton_obj_iff_of_nonDegenerate, TwoSidedIdeal.asIdeal_jacobson, IsArtinian.monotone_stabilizes, prod_coe, OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom, OmegaCompletePartialOrder.ContinuousHom.coe_mk, abs_mul_sign, TwoSidedIdeal.mem_fromIdeal, PartOrd.coe_comp, partialSups_eq_sUnion_image, FiniteMulArchimedeanClass.liftOrderHom_mk, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, CategoryTheory.SimplicialThickening.functor_map, SSet.stdSimplex.coe_edge_down_toOrderHom, FirstOrder.Language.DirectLimit.liftInclusion_of, RelHom.toOrderHom_coe, addRothNumber_le_ruzsaSzemerediNumber, Finset.eraseNone_map_some, SemilatInfCat.coe_forget_to_partOrd, TwoSidedIdeal.mem_comap, hasStrictDerivAt_abs, TwoSidedIdeal.mem_asIdealOpposite, LinearMap.iterateKer_coe, addRothNumber_empty, CategoryTheory.antitone_chain_condition_of_isArtinianObject, Module.End.disjoint_genEigenspace, SSet.skeleton_succ, partOrdEmb_dual_comp_forget_to_pardOrd, CategoryTheory.Limits.kernelOrderHom_coe, rothNumberNat_def, addRothNumber_lt_of_forall_not_threeAPFree, Submodule.inf_iSup_genEigenspace, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, PartOrd.comp_apply, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Orientation.oangle_sign_smul_left, SimplexCategory.II.castSucc_mem_finset_iff, Pi.ฯScottContinuous_uncurry, RingEquiv.mapTwoSidedIdeal_apply, lfp_lfp, partialSups_eq_biSup, SimplexCategory.mono_iff_injective, Orientation.oangle_sign_smul_add_smul_smul_add_smul, eventually_nhdsWithin_sign_eq_of_deriv_pos, le_lfp, OrdinalApprox.gfpApprox_ord_eq_gfp, canLift, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_obj_carrier, SimplexCategory.II.map'_eq_last_iff, Module.End.mem_genEigenspace_top, rothNumberNat_isLittleO_id, sign_mul, Module.End.injOn_genEigenspace, isFixedPt_lfp, coe_mk, Module.End.genEigenspace_one, gfp_gfp, NonemptyInterval.map_snd, ThreeAPFree.le_rothNumberNat, addRothNumber_singleton, Preord.forget_map, EReal.sign_bot, SimplexCategory.rev_map_apply, bot_def, self_mul_sign, biUnion_Iic_disjointed, IsMulFreimanIso.mulRothNumber_congr, SimplexCategory.mkOfSucc_homToOrderHom_zero, CategoryTheory.monotone_chain_condition_of_isNoetherianObject, coe_iInf, Finset.sum_eraseNone, SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, ContinuousWithinAt.partialSups, apply_coe, CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app, Finset.coe_eraseNone, MeasureTheory.IsSetRing.partialSups_mem, apply_mono, le_mulRothNumber_product, sign_apply, equivalenceFunctor_functor_obj_obj, ContinuousOn.partialSups, DivisibleHull.qsmul_def, sign_one, PartOrd.inv_hom_apply, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, ciSup_partialSups_eq, ThreeAPFree.le_addRothNumber, CategoryTheory.isNoetherianObject_iff_monotone_chain_condition, SimplexCategory.II.map'_eq_castSucc_iff, curry_apply, TwoSidedIdeal.comap_comap, LinOrd.forget_map, Affine.Simplex.ExcenterExists.sign_touchpointWeights, le_monotonicSequenceLimit, SSet.prodStdSimplex.objEquiv_map_apply, Fin.predAboveOrderHom_coe, LinOrd.ext_iff, Affine.Simplex.sign_touchpointWeights_singleton_pos, ContinuousAt.partialSups, Orientation.oangle_sign_smul_right, mono, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, partialSups_zero, wellFoundedGT_iff_monotone_chain_condition, mulRothNumber_empty, CategoryTheory.Limits.FormalCoproduct.cech_map, monotone_stabilizes_iff_noetherian, BoxIntegral.Box.Ioo_subset_Icc, BoxIntegral.Box.exists_seq_mono_tendsto, SSet.stdSimplex.const_down_toOrderHom, Heyting.Regular.coe_toRegular, Pi.monotoneUncurry_coe, Behrend.card_sphere_le_rothNumberNat, Part.fix_eq_ฯSup, map_partialSups, rothNumberNat_le_ruzsaSzemerediNumberNat, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, ext_iff, sign_neg, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_obj_isFintype, map_gfp, signedDist_smul, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, SimplexCategoryGenRel.simplicialEvalฯ_of_isAdmissible, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, toFun_eq_coe, SSet.skeletonOfMono_zero, Affine.Simplex.sign_touchpointWeights_singleton_neg, addRothNumber_map_add_left, rothNumberNat_add_le, Module.End.genEigenspace_zero_nat, TwoSidedIdeal.top_asIdeal, TwoSidedIdeal.mem_asIdeal, EReal.sign_top, Finset.eraseNone_eq_biUnion, Module.End.genEigenspace_top, SSet.spine_map_vertex, fderiv_norm_smul, Part.ฯScottContinuous_toUnitMono, Ideal.asIdeal_toTwoSided, HasFDerivAt.hasFDerivAt_norm_smul, NonemptyFinLinOrd.id_apply, Affine.Simplex.sign_signedInfDist_touchpoint_empty, sign_nonpos_iff, disjoint_partialSups_left, Preord.coe_comp, sign_pow, StrictMono.sign_comp, SSet.mem_skeleton, hasDerivAt_abs, coe_inf, SSet.iSup_skeletonOfMono, Affine.Simplex.sign_excenterWeights_empty, Pi.monotoneCurry_coe, Part.Fix.le_f_of_mem_approx, SimplexCategory.II.mem_finset_iff, Interval.map_pure, isGreatest_gfp_le, Lat_dual_comp_forget_to_partOrd, Monotone.partialSups_eq, sign_eq_zero_iff, SSet.skeletonOfMono_obj_eq_top, comp_coe, CategoryTheory.isArtinianObject_iff_antitone_chain_condition, FinPartOrd.comp_apply, SSet.stdSimplex.objEquiv_toOrderHom_apply, upperBounds_range_partialSups, partialSups_eq_ciSup_Iic, Fin.addRothNumber_le_rothNumberNat, SimplexCategory.const_apply, AugmentedSimplexCategory.inl'_eval, EReal.le_iff_sign, antisymmetrization_apply_mk, ThreeGPFree.mulRothNumber_eq, LinOrd.coe_id, partialSups_iff_forall, NonemptyInterval.map_fst, Finset.prod_eraseNone, Set.partialSups_eq_accumulate, diag_coe, Finset.eraseNone_image_some, Module.End.generalized_eigenvec_disjoint_range_ker, coe_eq, NonemptyFinLinOrd.comp_apply, OmegaCompletePartialOrder.Chain.exists_of_mem_map, IsAddFreimanIso.addRothNumber_congr, DivisibleHull.archimedeanClassOrderIso_apply, addRothNumber_le, continuousAt_sign_of_neg, disjointed_succ, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, OrderHomClass.coe_coe, Module.End.mem_genEigenspace_one, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', uliftMap_coe_down, preordToCat_map, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, IsAddFreimanHom.addRothNumber_mono, SSet.stdSimplex.objMk_apply, fst_coe, Module.End.genEigenspace_div, LinearMap.iterateRange_coe, OmegaCompletePartialOrder.Chain.map_coe, SimplexCategory.toType_apply, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, curry_symm_apply, SimplexCategory.toCat_obj, continuousAt_sign_of_pos, CategoryTheory.Arrow.cechNerve_map, prodโ_coe_coe_coe, CircleDeg1Lift.coe_toOrderHom, SimplexCategory.concreteCategoryHom_id, Heyting.Regular.toRegular_coe, NonemptyInterval.subset_coe_map, eventuallyConst_of_isNoetherian, TwoSidedIdeal.gc, mulRothNumber_le, Part.Fix.approx_mono', Continuous.partialSups_apply, Module.End.genEigenspace_nat, Finset.eraseNone_inter, Affine.Simplex.ExcenterExists.signedInfDist_excenter, CategoryTheory.Arrow.cechConerve_map, Real.Angle.sign_toReal, coeFnHom_coe, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, sign_eq_sign_or_eq_neg, ContinuousOn.partialSups_apply, const_coe_coe, Module.End.genEigenspace_le_maximal, CategoryTheory.Functor.WellOrderInductionData.map_lift, monotone_stabilizes_iff_artinian, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, dual_apply_coe, Module.End.mem_genEigenspace_nat, uliftLeftMap_coe, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, EReal.sign_mul_inv_abs, BoxIntegral.Box.measurableSet_Ioo, Behrend.bound_aux, MeasureTheory.OuterMeasure.isCaratheodory_partialSups, Submodule.mem_iSup_of_chain, Affine.Simplex.sign_signedInfDist_incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, FinPartOrd_dual_comp_forget_to_partOrd, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, dual_symm_apply_coe, EReal.sign_mul_abs, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, WellFoundedGT.monotone_chain_condition', Orientation.oangle_sign_smul_add_smul_right, isGreatest_gfp, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, Polynomial.signVariations_eq_eraseLead_add_ite, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_map, idealFactorsFunOfQuotHom_coe_coe, PartOrd.hom_inv_apply, Pi.ฯScottContinuous_curry, OmegaCompletePartialOrder.ContinuousHom.coe_apply, OrdinalApprox.lfp_mem_range_lfpApprox, ArchimedeanClass.orderHom_top, FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, partialSups_bot, TwoSidedIdeal.orderIsoIsTwoSided_apply_coe, TwoSidedIdeal.asIdeal_matrix, OmegaCompletePartialOrder.ContinuousHom.toMono_coe, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, Continuous.partialSups, le_partialSups, iSup_apply, Pi.uncurry_curry_ฯScottContinuous, wellFoundedGT_iff_monotone_chain_condition', Part.Fix.mem_iff, EReal.sign_neg, partialSups_eq_biUnion_range, addRothNumber_Ico, ArchimedeanClass.liftOrderHom_mk, ArchimedeanClass.orderHom_mk, Pi.evalOrderHom_coe, PartOrd.forget_map, mulRothNumber_lt_of_forall_not_threeGPFree, sInf_apply, Module.End.hasGenEigenvector_iff, MulArchimedeanClass.orderHom_mk, SemilatSupCat_dual_comp_forget_to_partOrd, CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit, Module.End.mem_genEigenspace_zero, withTopMap_coe, Int.sign_eq_sign, addRothNumber_map_add_right, PartOrd.ofHom_apply, Finset.card_eraseNone_eq_card_erase, Preord.comp_apply, rothNumberNat_le_ruzsaSzemerediNumberNat', CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, linOrd_dual_comp_forget_to_Lat, onDiag_coe, AugmentedSimplexCategory.inr'_eval, Module.End.genEigenspace_le_genEigenspace_finrank, OrderAddMonoidIso.coe_orderIso, Module.End.mem_genEigenspace, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, OmegaCompletePartialOrder.Chain.mem_map_iff, uliftRightMap_coe_down, partialSups_add_one_eq_sup_disjointed, compโ_coe_coe_coe, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_obj_str, SimplexCategory.toCat_map, NonemptyFinLinOrd.mono_iff_injective, Orientation.oangle_sign_smul_add_smul_left, Module.End.genEigenspace_zero, OrderMonoidHom.coe_orderHom, CategoryTheory.Limits.FormalCoproduct.cech_obj, mulRothNumber_map_mul_right, map_inf_fixedPoints_le, continuousAt_sign_of_ne_zero, OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ฯSup_coe, partialSups_le_iff, SSet.stdSimplex.objEquiv_symm_apply, SemilatSupCat.coe_forget_to_partOrd, Right.sign_neg, bddAbove_range_partialSups, LinOrd.comp_apply, LinOrd.coe_comp, partOrd_dual_comp_forget_to_preord, Module.End.genEigenspace_le_smul, mulRothNumber_union_le, isFixedPt_gfp, disjointed_partialSups, CategoryTheory.Limits.cokernelOrderHom_coe, isLeast_lfp_le, Finset.mem_eraseNone, coe_iSup, iterate_sup_le_sup_iff, Module.End.genEigenspace_restrict, CategoryTheory.SimplicialThickening.functor_obj_as, PartOrd.ext_iff, SimplexCategory.epi_iff_surjective, map_lfp_comp, Left.sign_neg, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, FinPartOrd.id_apply, Filter.Tendsto.partialSups, partialSups_add_const, Finset.eraseNone_empty, Finset.eraseNone_insertNone, EReal.sign_mul_inv_abs', Finset.disjiUnion_Iic_disjointed, sign_eq_neg_one_iff, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, partialSups_disjoint_of_disjoint, coe_sup, sign_eq_one_iff, PartOrd.id_apply, ContinuousAt.partialSups_apply, RelEmbedding.toOrderHom_injective, TwoSidedIdeal.coe_asIdeal, partBind_coe, Finset.map_some_eraseNone, map_gfp_comp, FirstOrder.Language.DirectLimit.le_partialEquivLimit, MulArchimedeanClass.orderHom_top, Part.Fix.approx_mono, Pi.partialSups_apply, const_comp, PseudoEpimorphism.toOrderHom_eq_coe, FirstOrder.Language.DirectLimit.rangeLiftInclusion, TwoSidedIdeal.comap_le_comap, SSet.skeletonOfMono_succ, ArchimedeanClass.orderHom_injective, instOrderHomClass, Submodule.coe_iSup_of_chain, FirstOrder.Language.DirectLimit.dom_partialEquivLimit, mulRothNumber_singleton, SSet.skeleton_zero
|
instInhabited ๐ | CompOp | โ |
instPartialOrder ๐ | CompOp | โ |
instPreorder ๐ | CompOp | 63 mathmath: partialSups_mono, OrderIso.arrowCongr_apply, OmegaCompletePartialOrder.ContinuousHom.ฯSup_apply, OrdinalApprox.gfp_mem_range_gfpApprox, mk_le_mk, lfp_induction, piIso_symm_apply, lfp_le_gfp, OmegaCompletePartialOrder.OrderHom.ฯSup_coe, map_lfp, top_def, gfp_const_inf_le, prodIso_apply, coe_le_coe, equivalenceFunctor_counitIso_inv_app_app, comp_const, le_def, isLeast_lfp, OrdinalApprox.lfpApprox_ord_eq_lfp, gfp_le, OrderIso.arrowCongr_symm_apply, lfp_lfp, le_lfp, OrdinalApprox.gfpApprox_ord_eq_gfp, isFixedPt_lfp, gfp_gfp, bot_def, apply_coe, equivalenceFunctor_functor_obj_obj, OrdinalApprox.lfpApprox_mono_left, curry_apply, OrderIso.conj_symm_apply, SSet.stdSimplex.const_down_toOrderHom, map_gfp, equivalenceFunctor_counitIso_hom_app_app, equivalenceFunctor_unitIso_hom_app, isGreatest_gfp_le, equivalenceFunctor_inverse_obj, OrdinalApprox.gfpApprox_mono_left, fixedPoints.lfp_eq_sSup_iterate, curry_symm_apply, prodโ_coe_coe_coe, coeFnHom_coe, const_coe_coe, fixedPoints.gfp_eq_sInf_iterate, isGreatest_gfp, gfp_induction, OrdinalApprox.lfp_mem_range_lfpApprox, OmegaCompletePartialOrder.ContinuousHom.toMono_coe, prodIso_symm_apply, piIso_apply, lfp_le, onDiag_coe, equivalenceFunctor_unitIso_inv_app, compโ_coe_coe_coe, OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ฯSup_coe, isFixedPt_gfp, isLeast_lfp_le, map_lfp_comp, lfp_le_fixed, le_gfp, map_gfp_comp, const_comp
|
onDiag ๐ | CompOp | 3 mathmath: lfp_lfp, gfp_gfp, onDiag_coe
|
pi ๐ | CompOp | 2 mathmath: piIso_symm_apply, pi_coe
|
piIso ๐ | CompOp | 2 mathmath: piIso_symm_apply, piIso_apply
|
prod ๐ | CompOp | 7 mathmath: prod_coe, comp_prod_comp_same, snd_comp_prod, prod_mono, fst_prod_snd, fst_comp_prod, prodIso_symm_apply
|
prodIso ๐ | CompOp | 2 mathmath: prodIso_apply, prodIso_symm_apply
|
prodMap ๐ | CompOp | 1 mathmath: prodMap_coe
|
prodโ ๐ | CompOp | 1 mathmath: prodโ_coe_coe_coe
|
snd ๐ | CompOp | 6 mathmath: prodIso_apply, snd_coe, snd_comp_prod, fst_prod_snd, Prod.ฯSup_snd, Prod.ฯSupImpl_snd
|
toFun ๐ | CompOp | 15 mathmath: ClosureOperator.idempotent', PseudoEpimorphism.toFun_eq_coe, ContinuousOrderHom.continuous_toFun, CategoryTheory.Limits.FormalCoproduct.cech_map, toFun_eq_coe, ContinuousOrderHom.toFun_eq_coe, ClosureOperator.isClosed_iff, HahnSeries.embDomainOrderAddMonoidHom_apply, CircleDeg1Lift.map_add_one', ClosureOperator.le_closure', EsakiaHom.toFun_eq_coe, BoundedOrderHom.map_top', BoundedOrderHom.map_bot', OmegaCompletePartialOrder.ContinuousHom.map_ฯSup', monotone'
|
uliftLeftMap ๐ | CompOp | 3 mathmath: uliftLeftMap_uliftRightMap_eq, uliftRightMap_uliftLeftMap_eq, uliftLeftMap_coe
|
uliftMap ๐ | CompOp | 3 mathmath: uliftLeftMap_uliftRightMap_eq, uliftRightMap_uliftLeftMap_eq, uliftMap_coe_down
|
uliftRightMap ๐ | CompOp | 3 mathmath: uliftLeftMap_uliftRightMap_eq, uliftRightMap_uliftLeftMap_eq, uliftRightMap_coe_down
|
unique ๐ | CompOp | โ |
| Name | Category | Theorems |
|---|
arrowCongr ๐ | CompOp | 3 mathmath: arrowCongr_apply, arrowCongr_symm_apply, conj_symm_apply
|
conj ๐ | CompOp | 3 mathmath: ClosureOperator.conjBy_apply, conj_apply, conj_symm_apply
|
dual ๐ | CompOp | 3 mathmath: dual_apply, dual_symm_apply, symm_dual
|
dualDual ๐ | CompOp | 6 mathmath: coe_dualDual_symm, FinPartOrd.dualEquiv_unitIso, dualDual_apply, coe_dualDual, FinPartOrd.dualEquiv_counitIso, dualDual_symm_apply
|
funUnique ๐ | CompOp | 3 mathmath: funUnique_toEquiv, funUnique_apply, funUnique_symm_apply
|
instEquivLike ๐ | CompOp | 12 mathmath: sumCongr_apply, Sublattice.map_equiv_eq_comap_symm, instHomeomorphClass, Finpartition.parts_map, Real.sinhHomeomorph_symm_apply, sumLexCongr_apply, instOrderIsoClass, conj_symm_apply, Sublattice.comap_equiv_eq_map_symm, Sublattice.map_symm_eq_iff_eq_map, Prod.Lex.prodLexCongr_apply, Sublattice.mem_map_equiv
|
ofCmpEqCmp ๐ | CompOp | โ |
ofHomInv ๐ | CompOp | 2 mathmath: ofHomInv_apply, ofHomInv_symm_apply
|
ofIsEmpty ๐ | CompOp | โ |
ofRelIsoLT ๐ | CompOp | 4 mathmath: ofRelIsoLT_apply, toRelIsoLT_ofRelIsoLT, ofRelIsoLT_symm, ofRelIsoLT_toRelIsoLT
|
ofUnique ๐ | CompOp | 2 mathmath: ofUnique_symm_apply, ofUnique_apply
|
prodAssoc ๐ | CompOp | 2 mathmath: prodAssoc_apply, prodAssoc_symm_apply
|
prodComm ๐ | CompOp | 2 mathmath: coe_prodComm, prodComm_symm
|
refl ๐ | CompOp | 17 mathmath: withTopCongr_refl, refl_apply, UpperSet.map_refl, refl_toEquiv, withBotCongr_refl, coe_refl, sumLexCongr_refl, symm_trans_self, Fin.castOrderIso_refl, LowerSet.map_refl, refl_trans, symm_refl, ClosureOperator.conjBy_refl, sumCongr_refl, trans_refl, self_trans_symm, OrderRingIso.coe_orderIso_refl
|
toOrderEmbedding ๐ | CompOp | 5 mathmath: AugmentedSimplexCategory.eqToHom_toOrderHom, SSet.stdSimplex.face_eq_ofSimplex, coe_toOrderEmbedding, SimplexCategory.eqToHom_toOrderHom, Finset.orderEmbOfFin_compl_singleton
|
toRelIsoGT ๐ | CompOp | 4 mathmath: toRelIsoGT_symm, coe_symm_toRelIsoGT, coe_toRelIsoGT, toRelIsoGT_apply
|
toRelIsoLT ๐ | CompOp | 6 mathmath: toRelIsoLT_symm, toRelIsoLT_apply, coe_toRelIsoLT, toRelIsoLT_ofRelIsoLT, coe_symm_toRelIsoLT, ofRelIsoLT_toRelIsoLT
|
trans ๐ | CompOp | 17 mathmath: symm_trans, symm_trans_apply, UpperSet.map_map, OrderAddMonoidIso.coe_trans_orderIso, sumLexCongr_trans, withTopCongr_trans, trans_apply, sumCongr_trans, OrderMonoidIso.coe_trans_orderIso, symm_trans_self, ClosureOperator.conjBy_trans, coe_trans, refl_trans, withBotCongr_trans, trans_refl, LowerSet.map_map, self_trans_symm
|
| Name | Category | Theorems |
|---|
OrderHom ๐ | CompData | 595 mathmath: Behrend.roth_lower_bound, partialSups_apply, HurwitzZeta.hasSum_int_hurwitzZetaOdd, sign_intCast, hasSum_mellin_pi_mul_sq', rothNumberNat_spec, NonemptyInterval.dual_map, LinearMap.iterateRange_succ, SSet.stdSimplex.coe_triangle_down_toOrderHom, SimplexCategory.eq_const_of_zero, sign_mul_self, NonemptyInterval.map_pure, partialSups_const_add, LinOrd.ofHom_apply, partialSups_succ', partialSups_mono, OrderIso.arrowCongr_apply, deriv_abs, OmegaCompletePartialOrder.ContinuousHom.ฯSup_apply, Affine.Simplex.sign_excenterWeights_singleton_pos, OrderHom.le_map_sup_fixedPoints, OrderHom.dual_id, SSet.ofSimplex_le_skeleton, Part.Fix.exists_fix_le_approx, OrdinalApprox.gfp_mem_range_gfpApprox, signHom_apply, WellFoundedGT.monotone_chain_condition, ciSup_partialSups_eq', CategoryTheory.Functor.toOrderHom_coe, Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, Fin.orderHom_injective_iff, SimplexCategory.const_comp, OrderHom.mk_le_mk, Module.End.independent_genEigenspace, le_addRothNumber_product, Behrend.roth_lower_bound_explicit, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, Filter.Tendsto.partialSups_apply, OrderAddMonoidHom.coe_orderHom, OrderHom.id_coe, OrderHom.piIso_symm_apply, rothNumberNat_le, partialSups_eq_sup'_range, MulArchimedeanClass.orderHom_injective, OrderHom.lfp_le_gfp, Part.toUnitMono_coe, Affine.Simplex.wSameSide_affineSpan_faceOpposite_iff, IsArtinian.eventuallyConst_of_isArtinian, OrderHom.monotone, TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, EReal.sign_eq_and_abs_eq_iff_eq, WellFoundedGT.iSup_eq_monotonicSequenceLimit, OmegaCompletePartialOrder.OrderHom.ฯSup_coe, Module.End.genEigenspace_directed, SSet.prodStdSimplex.orderHomOfSimplex_coe, sign_nonneg_iff, OrderHom.antisymmetrization_apply, LinOrd.dual_map, biUnion_range_succ_disjointed, OrderHom.map_lfp, Module.End.maxGenEigenspace_eq, SemilatInfCat_dual_comp_forget_to_partOrd, BoxIntegral.Box.Ioo_subset_coe, partialSups_add_one', OrderHom.top_def, Preord.coe_id, Behrend.bound_aux', OrderHom.gfp_const_inf_le, Affine.Simplex.sign_touchpointWeights_empty, TwoSidedIdeal.bot_asIdeal, Preord.ext_iff, OrderHom.coe_antisymmetrization, Part.Fix.approx_mem_approxChain, SSet.prodStdSimplex.objEquiv_apply_fst, ClosureOperator.conjBy_apply, iSup_partialSups_eq, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, mulRothNumber_map_mul_left, Prod.Lex.toLexOrderHom_coe, OrderHom.prodIso_apply, Preord.inv_hom_apply, Module.End.mapsTo_genEigenspace_of_comm, partialSups_const_mul, OrderHom.snd_coe, OrderHom.iInf_apply, Preord.hom_inv_apply, Part.Fix.approx_le_fix, HasStrictFDerivAt.abs, Ideal.toTwoSided_asIdeal, NonemptyFinLinOrd.epi_iff_surjective, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, LinOrd.hom_inv_apply, SSet.iSup_skeleton, partialSups_add_one, Finset.insertNone_eraseNone, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkOfSucc_homToOrderHom_one, OrderHom.sSup_apply, OrderHom.Subtype.val_coe, SimplexCategory.Hom.mk_toOrderHom_apply, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, OrderHom.coe_le_coe, SSet.prodStdSimplex.strictMono_orderHomOfSimplex_iff, PartOrd.coe_id, OrderHom.equivalenceFunctor_counitIso_inv_app_app, Preord.ofHom_apply, BoundedOrderHom.dual_apply_toOrderHom, hasDerivWithinAt_abs, SSet.skeleton_le_skeletonOfMono, SSet.prodStdSimplex.objEquiv_ฮด_apply, Finset.card_eraseNone_le, EReal.abs_mul_sign, Finset.eraseNone_union, PartOrd.dual_map, mulRothNumber_spec, Finset.eraseNone_none, LinOrd.inv_hom_apply, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac, SSet.prodStdSimplex.objEquiv_naturality, Submodule.inf_genEigenspace, OrderHom.withBotMap_coe, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, ThreeAPFree.addRothNumber_eq, sign_zero, disjoint_partialSups_right, OrderHom.comp_const, SimplexCategory.toTop_map, ArchimedeanClass.orderHom_zero, NormedSpace.normalize_smul, sign_mul_abs, sign_eq_of_affineCombination_mem_affineSpan_single_lineMap, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, MulArchimedeanClass.liftOrderHom_mk, BoxIntegral.Box.iUnion_Ioo_of_tendsto, OrderHom.prodMap_coe, ContinuousWithinAt.partialSups_apply, addRothNumber_union_le, Interval.subset_coe_map, sign_pos, le_partialSups_of_le, OmegaCompletePartialOrder.Chain.mem_map, comp_partialSups, Finset.card_eraseNone_of_not_mem, SimplexCategory.toTopโ_map, CircleDeg1Lift.coe_mk, SSet.prodStdSimplex.objEquiv_apply_snd, LinearMap.finrank_genEigenspace_le, partialSups_eq_sup_range, SimplexCategory.congr_toOrderHom_apply, HasFDerivAt.abs, HasFDerivWithinAt.abs, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, Module.End.iSup_genEigenspace_eq, OrderHom.le_def, Finset.card_eraseNone_of_mem, LinOrd.id_apply, Module.End.genEigenspace_inf_le_add, FiniteArchimedeanClass.liftOrderHom_mk, partialSups_monotone, Module.End.eigenspace_le_genEigenspace, rothNumberNat_zero, Affine.Simplex.wOppSide_affineSpan_faceOpposite_iff, BoxIntegral.Box.Ioo_ae_eq_Icc, FinBoolAlg.forgetToFinPartOrdFaithful, Fin.addRothNumber_eq_rothNumberNat, IsMulFreimanHom.mulRothNumber_mono, OrderHom.symm_dual_id, SSet.horn_obj, disjointed_add_one, SSet.skeleton_obj_eq_top, partialSups_mul_const, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, Preord.id_apply, OrderMonoidIso.coe_orderIso, EReal.sign_mul, OrderHom.isLeast_lfp, ContinuousOrderHom.coe_toOrderHom, bddOrd_dual_comp_forget_to_partOrd, partialSups_succ, EReal.sign_coe, SSet.stdSimplex.face_obj, Affine.Simplex.sign_excenterWeights_singleton_neg, OrderHom.pi_coe, partialSups_le, Finset.image_some_eraseNone, ThreeGPFree.le_mulRothNumber, SSet.Truncated.spine_map_vertex, OrderIso.conj_apply, OrdinalApprox.lfpApprox_ord_eq_lfp, classifyingSpaceUniversalCover_map, OrderHom.gfp_le, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, addRothNumber_spec, eventually_nhdsWithin_sign_eq_of_deriv_neg, OmegaCompletePartialOrder.ฯScottContinuous_iff_map_ฯSup_of_orderHom, SSet.mem_skeleton_obj_iff_of_nonDegenerate, TwoSidedIdeal.asIdeal_jacobson, IsArtinian.monotone_stabilizes, OrderHom.prod_coe, OmegaCompletePartialOrder.ContinuousHom.coe_toOrderHom, OmegaCompletePartialOrder.ContinuousHom.coe_mk, abs_mul_sign, TwoSidedIdeal.mem_fromIdeal, PartOrd.coe_comp, partialSups_eq_sUnion_image, OrderIso.arrowCongr_symm_apply, FiniteMulArchimedeanClass.liftOrderHom_mk, HurwitzZeta.hasSum_int_completedHurwitzZetaOdd, CategoryTheory.SimplicialThickening.functor_map, SSet.stdSimplex.coe_edge_down_toOrderHom, FirstOrder.Language.DirectLimit.liftInclusion_of, RelHom.toOrderHom_coe, addRothNumber_le_ruzsaSzemerediNumber, Finset.eraseNone_map_some, SemilatInfCat.coe_forget_to_partOrd, TwoSidedIdeal.mem_comap, hasStrictDerivAt_abs, TwoSidedIdeal.mem_asIdealOpposite, LinearMap.iterateKer_coe, addRothNumber_empty, CategoryTheory.antitone_chain_condition_of_isArtinianObject, Module.End.disjoint_genEigenspace, SSet.skeleton_succ, partOrdEmb_dual_comp_forget_to_pardOrd, CategoryTheory.Limits.kernelOrderHom_coe, rothNumberNat_def, addRothNumber_lt_of_forall_not_threeAPFree, Submodule.inf_iSup_genEigenspace, nonemptyFinLinOrd_dual_comp_forget_to_linOrd, PartOrd.comp_apply, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Orientation.oangle_sign_smul_left, SimplexCategory.II.castSucc_mem_finset_iff, Pi.ฯScottContinuous_uncurry, RingEquiv.mapTwoSidedIdeal_apply, OrderHom.lfp_lfp, partialSups_eq_biSup, SimplexCategory.mono_iff_injective, Orientation.oangle_sign_smul_add_smul_smul_add_smul, eventually_nhdsWithin_sign_eq_of_deriv_pos, OrderHom.le_lfp, OrdinalApprox.gfpApprox_ord_eq_gfp, FinPartOrd.dual_map, OrderHom.canLift, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_obj_carrier, SimplexCategory.II.map'_eq_last_iff, Module.End.mem_genEigenspace_top, rothNumberNat_isLittleO_id, sign_mul, Module.End.injOn_genEigenspace, OrderHom.isFixedPt_lfp, OrderHom.coe_mk, Module.End.genEigenspace_one, OrderHom.gfp_gfp, NonemptyInterval.map_snd, ThreeAPFree.le_rothNumberNat, addRothNumber_singleton, Preord.forget_map, EReal.sign_bot, SimplexCategory.rev_map_apply, OrderHom.bot_def, self_mul_sign, biUnion_Iic_disjointed, IsMulFreimanIso.mulRothNumber_congr, SimplexCategory.mkOfSucc_homToOrderHom_zero, CategoryTheory.monotone_chain_condition_of_isNoetherianObject, OrderHom.coe_iInf, Finset.sum_eraseNone, SimplexCategory.instReflectsIsomorphismsForgetOrderHomFinHAddNatLenOfNat, ContinuousWithinAt.partialSups, OrderHom.apply_coe, CategoryTheory.Limits.FormalCoproduct.cechFunctor_map_app, Finset.coe_eraseNone, MeasureTheory.IsSetRing.partialSups_mem, le_mulRothNumber_product, sign_apply, OrderHom.equivalenceFunctor_functor_obj_obj, OrderHom.dual_comp, ContinuousOn.partialSups, DivisibleHull.qsmul_def, sign_one, PartOrd.inv_hom_apply, OrdinalApprox.lfpApprox_mono_left, Affine.Simplex.sSameSide_affineSpan_faceOpposite_iff, ciSup_partialSups_eq, ThreeAPFree.le_addRothNumber, CategoryTheory.isNoetherianObject_iff_monotone_chain_condition, SimplexCategory.II.map'_eq_castSucc_iff, OrderHom.curry_apply, TwoSidedIdeal.comap_comap, LinOrd.forget_map, Affine.Simplex.ExcenterExists.sign_touchpointWeights, le_monotonicSequenceLimit, SSet.prodStdSimplex.objEquiv_map_apply, Fin.predAboveOrderHom_coe, LinOrd.ext_iff, Affine.Simplex.sign_touchpointWeights_singleton_pos, ContinuousAt.partialSups, Orientation.oangle_sign_smul_right, OrderHom.mono, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, partialSups_zero, wellFoundedGT_iff_monotone_chain_condition, mulRothNumber_empty, CategoryTheory.Limits.FormalCoproduct.cech_map, OrderIso.conj_symm_apply, monotone_stabilizes_iff_noetherian, BoxIntegral.Box.Ioo_subset_Icc, NonemptyFinLinOrd.dual_map, BoxIntegral.Box.exists_seq_mono_tendsto, SSet.stdSimplex.const_down_toOrderHom, Heyting.Regular.coe_toRegular, Pi.monotoneUncurry_coe, Behrend.card_sphere_le_rothNumberNat, Part.fix_eq_ฯSup, map_partialSups, rothNumberNat_le_ruzsaSzemerediNumberNat, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, OrderHom.ext_iff, sign_neg, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_obj_isFintype, OrderHom.map_gfp, signedDist_smul, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, SimplexCategoryGenRel.simplicialEvalฯ_of_isAdmissible, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, HurwitzZeta.hasSum_nat_hurwitzZetaOdd, OrderHom.toFun_eq_coe, SSet.skeletonOfMono_zero, Affine.Simplex.sign_touchpointWeights_singleton_neg, addRothNumber_map_add_left, OrderAddMonoidHom.toOrderHom_injective, rothNumberNat_add_le, Preord.dual_map, Module.End.genEigenspace_zero_nat, TwoSidedIdeal.top_asIdeal, TwoSidedIdeal.mem_asIdeal, EReal.sign_top, OrderHom.equivFunctor_apply, Finset.eraseNone_eq_biUnion, Module.End.genEigenspace_top, SSet.spine_map_vertex, fderiv_norm_smul, Part.ฯScottContinuous_toUnitMono, OrderHom.equivalenceFunctor_counitIso_hom_app_app, Ideal.asIdeal_toTwoSided, HasFDerivAt.hasFDerivAt_norm_smul, NonemptyFinLinOrd.id_apply, Affine.Simplex.sign_signedInfDist_touchpoint_empty, sign_nonpos_iff, disjoint_partialSups_left, Preord.coe_comp, sign_pow, OrderHom.equivalenceFunctor_unitIso_hom_app, StrictMono.sign_comp, SSet.mem_skeleton, hasDerivAt_abs, OrderHom.coe_inf, SSet.iSup_skeletonOfMono, Affine.Simplex.sign_excenterWeights_empty, Pi.monotoneCurry_coe, Part.Fix.le_f_of_mem_approx, SimplexCategory.II.mem_finset_iff, Interval.map_pure, OrderHom.isGreatest_gfp_le, Lat_dual_comp_forget_to_partOrd, Monotone.partialSups_eq, sign_eq_zero_iff, SSet.skeletonOfMono_obj_eq_top, OrderHom.comp_coe, CategoryTheory.isArtinianObject_iff_antitone_chain_condition, FinPartOrd.comp_apply, SSet.stdSimplex.objEquiv_toOrderHom_apply, upperBounds_range_partialSups, partialSups_eq_ciSup_Iic, Fin.addRothNumber_le_rothNumberNat, SimplexCategory.const_apply, AugmentedSimplexCategory.inl'_eval, BoundedOrderHom.dual_symm_apply_toOrderHom, EReal.le_iff_sign, OrderHom.antisymmetrization_apply_mk, ThreeGPFree.mulRothNumber_eq, LinOrd.coe_id, partialSups_iff_forall, NonemptyInterval.map_fst, Finset.prod_eraseNone, Set.partialSups_eq_accumulate, OrderHom.diag_coe, Finset.eraseNone_image_some, Module.End.generalized_eigenvec_disjoint_range_ker, OrderHom.coe_eq, NonemptyFinLinOrd.comp_apply, OmegaCompletePartialOrder.Chain.exists_of_mem_map, IsAddFreimanIso.addRothNumber_congr, OrderHom.equivalenceFunctor_inverse_obj, DivisibleHull.archimedeanClassOrderIso_apply, addRothNumber_le, continuousAt_sign_of_neg, disjointed_succ, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, OrderHomClass.coe_coe, Module.End.mem_genEigenspace_one, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', OrderHom.uliftMap_coe_down, preordToCat_map, OrdinalApprox.gfpApprox_mono_left, SSet.prodStdSimplex.nonDegenerate_iff_injective_objEquiv, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, IsAddFreimanHom.addRothNumber_mono, OrderHom.symm_dual_comp, SSet.stdSimplex.objMk_apply, OrderHom.fst_coe, Module.End.genEigenspace_div, LinearMap.iterateRange_coe, OmegaCompletePartialOrder.Chain.map_coe, SimplexCategory.toType_apply, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, OrderHom.curry_symm_apply, SimplexCategory.toCat_obj, continuousAt_sign_of_pos, CategoryTheory.Arrow.cechNerve_map, OrderHom.prodโ_coe_coe_coe, CircleDeg1Lift.coe_toOrderHom, SimplexCategory.concreteCategoryHom_id, Heyting.Regular.toRegular_coe, NonemptyInterval.subset_coe_map, eventuallyConst_of_isNoetherian, TwoSidedIdeal.gc, mulRothNumber_le, Part.Fix.approx_mono', Continuous.partialSups_apply, Module.End.genEigenspace_nat, Finset.eraseNone_inter, Affine.Simplex.ExcenterExists.signedInfDist_excenter, CategoryTheory.Arrow.cechConerve_map, Real.Angle.sign_toReal, OrderHom.coeFnHom_coe, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, sign_eq_sign_or_eq_neg, ContinuousOn.partialSups_apply, OrderHom.const_coe_coe, Module.End.genEigenspace_le_maximal, CategoryTheory.Functor.WellOrderInductionData.map_lift, monotone_stabilizes_iff_artinian, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureDomCoeOrderHomPartialEquivEmbeddingInclusion, OrderHom.dual_apply_coe, Module.End.mem_genEigenspace_nat, OrderHom.uliftLeftMap_coe, CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.map_lift, EReal.sign_mul_inv_abs, BoxIntegral.Box.measurableSet_Ioo, Behrend.bound_aux, MeasureTheory.OuterMeasure.isCaratheodory_partialSups, Submodule.mem_iSup_of_chain, Affine.Simplex.sign_signedInfDist_incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, FinPartOrd_dual_comp_forget_to_partOrd, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, OrderHom.dual_symm_apply_coe, EReal.sign_mul_abs, SSet.prodStdSimplex.nonDegenerate_iff_strictMono_objEquiv, WellFoundedGT.monotone_chain_condition', Orientation.oangle_sign_smul_add_smul_right, OrderHom.isGreatest_gfp, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, Polynomial.signVariations_eq_eraseLead_add_ite, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_map, idealFactorsFunOfQuotHom_coe_coe, PartOrd.hom_inv_apply, Pi.ฯScottContinuous_curry, OmegaCompletePartialOrder.ContinuousHom.coe_apply, OrdinalApprox.lfp_mem_range_lfpApprox, ArchimedeanClass.orderHom_top, FirstOrder.Language.instDirectedSystemSubtypeMemSubstructureCoeOrderHomEmbeddingInclusion, partialSups_bot, TwoSidedIdeal.orderIsoIsTwoSided_apply_coe, TwoSidedIdeal.asIdeal_matrix, OmegaCompletePartialOrder.ContinuousHom.toMono_coe, FirstOrder.Language.DirectLimit.instDirectedSystemSubtypeMemSubstructureCodCoeOrderHomPartialEquivEmbeddingInclusion, Continuous.partialSups, OrderHom.prodIso_symm_apply, le_partialSups, OrderHom.iSup_apply, Pi.uncurry_curry_ฯScottContinuous, wellFoundedGT_iff_monotone_chain_condition', Part.Fix.mem_iff, EReal.sign_neg, partialSups_eq_biUnion_range, addRothNumber_Ico, ArchimedeanClass.liftOrderHom_mk, ArchimedeanClass.orderHom_mk, OrderHom.piIso_apply, Pi.evalOrderHom_coe, Interval.dual_map, PartOrd.forget_map, mulRothNumber_lt_of_forall_not_threeGPFree, OrderHom.sInf_apply, Module.End.hasGenEigenvector_iff, MulArchimedeanClass.orderHom_mk, SemilatSupCat_dual_comp_forget_to_partOrd, OrderHom.equivFunctor_symm_apply, CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit, Module.End.mem_genEigenspace_zero, OrderHom.withTopMap_coe, Int.sign_eq_sign, addRothNumber_map_add_right, PartOrd.ofHom_apply, Finset.card_eraseNone_eq_card_erase, Preord.comp_apply, rothNumberNat_le_ruzsaSzemerediNumberNat', CategoryTheory.SimplicialObject.augmentedCechNerve_obj_left_map, linOrd_dual_comp_forget_to_Lat, OrderHom.onDiag_coe, AugmentedSimplexCategory.inr'_eval, OrderHom.equivalenceFunctor_unitIso_inv_app, Module.End.genEigenspace_le_genEigenspace_finrank, OrderAddMonoidIso.coe_orderIso, Module.End.mem_genEigenspace, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, OmegaCompletePartialOrder.Chain.mem_map_iff, OrderHom.uliftRightMap_coe_down, partialSups_add_one_eq_sup_disjointed, OrderHom.compโ_coe_coe_coe, FinBoolAlg.hasForgetToFinPartOrd_forgetโ_obj_str, SimplexCategory.toCat_map, NonemptyFinLinOrd.mono_iff_injective, Orientation.oangle_sign_smul_add_smul_left, Module.End.genEigenspace_zero, OrderMonoidHom.coe_orderHom, CategoryTheory.Limits.FormalCoproduct.cech_obj, mulRothNumber_map_mul_right, OrderHom.map_inf_fixedPoints_le, continuousAt_sign_of_ne_zero, OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder_ฯSup_coe, partialSups_le_iff, SSet.stdSimplex.objEquiv_symm_apply, SemilatSupCat.coe_forget_to_partOrd, Right.sign_neg, bddAbove_range_partialSups, LinOrd.comp_apply, LinOrd.coe_comp, partOrd_dual_comp_forget_to_preord, Module.End.genEigenspace_le_smul, mulRothNumber_union_le, OrderHom.isFixedPt_gfp, disjointed_partialSups, CategoryTheory.Limits.cokernelOrderHom_coe, OrderHom.isLeast_lfp_le, Finset.mem_eraseNone, OrderHom.coe_iSup, OrderHom.iterate_sup_le_sup_iff, Module.End.genEigenspace_restrict, CategoryTheory.SimplicialThickening.functor_obj_as, PartOrd.ext_iff, SimplexCategory.epi_iff_surjective, OrderHom.map_lfp_comp, Left.sign_neg, Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, FinPartOrd.id_apply, Filter.Tendsto.partialSups, partialSups_add_const, Finset.eraseNone_empty, Finset.eraseNone_insertNone, EReal.sign_mul_inv_abs', Finset.disjiUnion_Iic_disjointed, sign_eq_neg_one_iff, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, partialSups_disjoint_of_disjoint, OrderHom.coe_sup, sign_eq_one_iff, PartOrd.id_apply, ContinuousAt.partialSups_apply, RelEmbedding.toOrderHom_injective, TwoSidedIdeal.coe_asIdeal, OrderHom.partBind_coe, Finset.map_some_eraseNone, OrderHom.map_gfp_comp, FirstOrder.Language.DirectLimit.le_partialEquivLimit, MulArchimedeanClass.orderHom_top, Part.Fix.approx_mono, Pi.partialSups_apply, OrderHom.const_comp, PseudoEpimorphism.toOrderHom_eq_coe, OrderMonoidHom.toOrderHom_injective, FirstOrder.Language.DirectLimit.rangeLiftInclusion, TwoSidedIdeal.comap_le_comap, SSet.skeletonOfMono_succ, ArchimedeanClass.orderHom_injective, OrderHom.instOrderHomClass, Submodule.coe_iSup_of_chain, FirstOrder.Language.DirectLimit.dom_partialEquivLimit, mulRothNumber_singleton, SSet.skeleton_zero
|
OrderHomClass ๐ | MathDef | 21 mathmath: CircleDeg1Lift.instOrderHomClassReal, OrderHomClass.of_addMonoidHom, InfHomClass.toOrderHomClass, OmegaCompletePartialOrder.instOrderHomClassContinuousHom, OrderHomClass.of_map_cstarMatrix_nonneg, OrderMonoidHom.instOrderHomClass, OrderMonoidWithZeroHom.instOrderHomClass, OrderRingHom.instOrderHomClass, OmegaCompletePartialOrder.Chain.instOrderHomClassNat, SupHomClass.toOrderHomClass, StarRingHomClass.instOrderHomClass, InitialSeg.instOrderHomClassLt, CompletelyPositiveMapClass.instOrderHomClass, OrderHomClass.ofLinear, PositiveLinearMap.instOrderHomClass, OrderIsoClass.toOrderHomClass, OrderAddMonoidHom.instOrderHomClass, ContinuousOrderHomClass.toOrderHomClass, OrderHomClass.toOrderHomClassOrderDual, ClosureOperator.instOrderHomClass, OrderHom.instOrderHomClass
|
OrderIsoClass ๐ | CompData | 8 mathmath: StarRingEquivClass.instOrderIsoClass, OrderIsoClass.toOrderIsoClassOrderDual, OrderIso.instOrderIsoClass, OrderAddMonoidIso.instOrderIsoClass, OrderMonoidIso.instOrderIsoClass, instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass, OrderRingIso.instOrderIsoClass, FirstOrder.Language.StrongHomClass.toOrderIsoClass
|
instCoeTCOrderIsoOfOrderIsoClass ๐ | CompOp | โ |
instFunLikeOrderEmbedding ๐ | CompOp | 390 mathmath: Cardinal.aleph_le_beth, Set.IsPWO.exists_monotone_subseq, Ordinal.principal_add_omega, Field.Emb.Cardinal.equivLim_coherence, OrderEmbedding.supIrredLowerSet_apply, OrderEmbedding.sorted_ge_listMap, RightOrdContinuous.coe_toOrderEmbedding, integralClosure_le_span_dualBasis, OrderEmbedding.birkhoffFinset_inf, Subalgebra.toSubmodule_injective, BoxIntegral.TaggedPrepartition.tag_mem_Icc, Cardinal.aleph_succ, Finset.image_orderEmbOfFin_univ, OrderEmbedding.sorted_lt_listMap, finSumEquivOfFinset_inr, Finset.add_sum_eq_sum_insertNone, OrderEmbedding.monotone, Cardinal.aleph_pos, OrderEmbedding.le_map_sup, OrderEmbedding.image_Ioc, Ordinal.omega_lt_omega, Ordinal.omega0_lt_omega_one, Submodule.mulMap_one_right_eq, Finset.orderEmbOfFin_unique, Field.Emb.Cardinal.directed_filtration, BoxIntegral.Box.upper_mem_Icc, BoxIntegral.Box.measurableSet_Icc, OrderEmbedding.infIrredUpperSet_surjective, Cardinal.ord.orderEmbedding_coe, Ordinal.omega0_lt_preOmega_iff, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, Cardinal.lift_eq_aleph_one, Ordinal.card_le_aleph, Composition.embedding_comp_inv, Ordinal.omega_zero, Nat.orderEmbeddingOfSet_apply, InitialSeg.toOrderEmbedding_apply, OrderEmbedding.maximal_mem_image, Nat.coe_orderEmbeddingOfSet, IsChain.preimage_embedding, UnitAddTorus.mFourierSubalgebra_coe, Ordinal.toGame_lt_iff, IsChain.image_embedding_iff, Composition.blocksFun_sigmaCompositionAux, Ordinal.omega_le_omega, Finset.card_insertNone, OrderEmbedding.preimage_uIoc, Ordinal.isInitial_preOmega, OrderEmbedding.preimage_Ici, OrderEmbedding.preimage_Icc, Subalgebra.mulMap_toLinearMap, BoxIntegral.Box.le_iff_Icc, Submonoid.adjoin_eq_span_of_eq_span, Ordinal.toGame_one, OrderEmbedding.preimage_Iic, Ordinal.range_omega, BoxIntegral.Prepartition.card_filter_mem_Icc_le, Ordinal.cof_preOmega, OrderEmbedding.preimage_Ioc, Algebra.span_le_adjoin, Finset.orderEmbOfFin_eq_orderEmbOfFin_iff, Cardinal.preAleph_le_aleph, OrderEmbedding.coe_ofStrictMono, Set.PartiallyWellOrderedOn.exists_monotone_subseq, Finset.insertNone_eraseNone, OrderEmbedding.toOrderHom_coe, BoxIntegral.Box.isCompact_Icc, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, Subalgebra.mem_toSubmodule, Subalgebra.range_isScalarTower_toAlgHom, GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite, Cardinal.aleph_one_le_continuum, Algebra.toSubmodule_bot, Cardinal.aleph_mul_aleph0, CovBy.image, OrderEmbedding.coe_birkhoffFinset, PartOrdEmb.comp_apply, Algebra.sInf_toSubmodule, exists_increasing_or_nonincreasing_subseq, PartOrdEmb.hom_inv_apply, instFullFunctor, Cardinal.aleph_add_aleph, WithBot.Ico_bot_coe, Subalgebra.finrank_toSubmodule, BoxIntegral.Box.measure_Icc_lt_top, Ordinal.mem_range_omega_iff, Subalgebra.isIdempotentElem_toSubmodule, Cardinal.lt_omega_iff_card_lt, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, span_coeff_minpolyDiv, Cardinal.aleph1_le_lift, OrderEmbedding.image_Ioo, OrderEmbedding.minimal_mem_image, PartOrdEmb.Limits.CoconePt.fac_apply, Algebra.top_toSubmodule, Finset.coe_orderIsoOfFin_apply, Cardinal.le_aleph_ord, OrderEmbedding.sortedLT_listMap, OrderEmbedding.birkhoffSet_inf, exists_increasing_or_nonincreasing_subseq', cardinalInterFilter_aleph_one_iff, BoxIntegral.Box.coe_ae_eq_Icc, OrderEmbedding.strictMono, OrderEmbedding.infIrredUpperSet_apply, FirstOrder.Language.LHom.coe_substructureReduct, CompositionAsSet.blocks_partial_sum, BoxIntegral.Box.Ioo_ae_eq_Icc, OrderIso.coe_toOrderEmbedding, Submodule.toSubalgebra_toSubmodule, Composition.index_embedding, Cardinal.aleph_le_aleph, traceForm_dualSubmodule_adjoin, FractionalIdeal.adjoinIntegral_coe, Subalgebra.mul_toSubmodule, Algebra.adjoin_nonUnitalSubalgebra_eq_span, SetTheory.Game.birthday_ordinalToGame, PartOrdEmb.ofHom_apply, HahnSeries.embDomain_single, SetTheory.Game.le_birthday, Finset.orderEmbOfFin_zero, Finset.none_mem_insertNone, Finset.mul_prod_eq_prod_insertNone, Order.exists_orderEmbedding_insert, PartOrdEmb.Limits.cocone_ฮน_app, HahnSeries.embDomain_coeff, FractionalIdeal.isFractional_adjoin_integral, Cardinal.ord_aleph, Composition.boundary_zero, mem_integralClosure_iff_mem_fg, exists_orderEmbedding_covby_of_forall_covby_finite, Finset.orderEmbOfFin_last, FirstOrder.Language.Substructure.skolemโ_reduct_isElementary, Affine.Simplex.face_points, Finset.range_orderEmbOfFin, Subalgebra.adjoin_eq_span_basis, Ordinal.isNormal_preOmega, Field.Emb.Cardinal.equivSucc_coherence, Ordinal.preOmega_ofNat, BoxIntegral.Box.lower_mem_Icc, Finset.orderEmbOfFin_singleton, Ordinal.preOmega_le_omega, Cardinal.isRegular_aleph_succ, Finset.coe_coeEmb, Ordinal.principal_mul_omega, Cardinal.aleph1_lt_lift, Submodule.map_subtype_embedding_eq, DFinsupp.coe_orderEmbeddingToFun, Subalgebra.mul_toSubmodule_le, FiniteArchimedeanClass.subsemigroup_eq_addSubgroup, Module.Flat.instSubalgebraToSubmodule, OrderEmbedding.maximal_mem_image_iff, partOrdEmb_dual_comp_forget_to_pardOrd, Cardinal.isNormal_aleph, Algebra.adjoin_toSubmodule_le, Set.isPWO_iff_exists_monotone_subseq, exteriorPower.ฮนMultiDual_apply_ฮนMulti, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, OrderEmbedding.withTopMap_apply, Cardinal.lift_eq_aleph1, PartOrdEmb.coe_comp, BoxIntegral.Box.Icc_def, OrderEmbedding.preimage_uIcc, FirstOrder.Language.Substructure.reduct_withConstants, Algebra.inf_toSubmodule, BoxIntegral.Box.isBounded_Icc, Algebra.adjoin_eq_span_of_subset, Finset.sum_insertNone, Cardinal.aleph_max, Cardinal.ord_preAleph, Field.Emb.Cardinal.eq_bot_of_not_nonempty, Subalgebra.linearDisjoint_iff, Ordinal.omega0_lt_omega1, OrderEmbedding.supIrredLowerSet_surjective, PartOrdEmb.inv_hom_apply, Ordinal.mk_toPGame, Submodule.comapMkQOrderEmbedding_eq, Ordinal.preOmega_zero, Finset.orderEmbOfCardLe_mem, exteriorPower.pairingDual_apply_apply_eq_one, Ordinal.coe_preOmega, Subalgebra.map_toSubmodule, Ordinal.omega0_le_omega, FirstOrder.Language.order.instStrongHomClassOrderEmbedding, PartOrdEmb.id_apply, BoxIntegral.Box.mapsTo_insertNth_face_Icc, Ordinal.toGame_zero, IsAntichain.preimage_embedding, WellQuasiOrdered.exists_monotone_subseq, Submodule.span_range_natDegree_eq_adjoin, Cardinal.range_aleph, Finset.some_mem_insertNone, Algebra.iInf_toSubmodule, fourierSubalgebra_coe, OrderEmbedding.sortedGE_listMap, OrderEmbedding.preimage_Iio, BoxIntegral.Box.Ioo_subset_Icc, OrderEmbedding.image_setOf_maximal, Cardinal.aleph_one_le_lift, BoxIntegral.Box.exists_seq_mono_tendsto, Subalgebra.finiteDimensional_toSubmodule, Ordinal.isInitial_omega, PartOrdEmb.forget_map, LeftOrdContinuous.coe_toOrderEmbedding, Subalgebra.toSubmodule_toSubalgebra, Algebra.adjoin_union_coe_submodule, Submodule.mulMap_one_left_eq, OrderEmbedding.maximal_apply_mem_inter_range_iff, Cardinal.lift_le_aleph1, BoxIntegral.Box.diam_Icc_le_of_distortion_le, OrderEmbedding.birkhoffSet_sup, Composition.mem_range_embedding, Ordinal.toGame_nmul, fg_adjoin_of_finite, OrderEmbedding.image_setOf_minimal, Ordinal.le_preOmega_self, Ordinal.toGame_lf_iff, Composition.invEmbedding_comp, PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier, Algebra.adjoin_eq_span, CliffordAlgebra.even_toSubmodule, Algebra.toSubmodule_eq_top, Composition.mem_range_embedding_iff', Ordinal.card_omega, Cardinal.lift_aleph, Finset.orderEmbOfFin_apply, Ordinal.omega0_le_preOmega_iff, Subalgebra.pi_toSubsemiring, BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq, Ordinal.lift_preOmega, Cardinal.aleph0_le_aleph, Finset.intervalGapsWithin_snd_of_lt, NonemptyInterval.coe_coeHom, Set.powersetCard.mem_ofFinEmbEquiv_iff_mem_range, Ordinal.omega_strictMono, Finset.intervalGapsWithin_succ_fst_of_lt, BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le, OrderEmbedding.minimal_mem_image_iff, OrderEmbedding.gtEmbedding_apply, List.sublist_iff_exists_fin_orderEmbedding_get_eq, OrderEmbedding.preimage_Ico, Cardinal.aleph0_lt_aleph_one, Composition.ones_embedding, IsAntichain.image_embedding_iff, OrderEmbedding.orderIso_apply, PartOrdEmb.Hom.injective, Ordinal.toGame_inj, Subalgebra.coe_pi, OrderEmbedding.image_Icc, Cardinal.aleph_mul_aleph, IsAntichain.image_embedding, OrderEmbedding.minimal_apply_mem_inter_range_iff, SetTheory.Game.neg_birthday_le, Cardinal.isRegular_aleph_one, PartOrdEmb.Hom.le_iff_le, BoxIntegral.Box.Icc_eq_pi, Cardinal.lift_le_aleph_one, Finset.intervalGapsWithin_fst_of_lt_lt, Finset.prod_insertNone, Ordinal.preOmega_strictMono, Ordinal.principal_opow_omega, Ordinal.card_preOmega, OrderEmbedding.subtype_apply, WithTop.top_mem_insertTop, OrderEmbedding.coe_ofIsEmpty, Finset.insertNone_nonempty, Nat.nth_eq_orderEmbOfFin, BoxIntegral.Box.coe_subset_Icc, Cardinal.aleph1_eq_lift, Composition.disjoint_range, OrderEmbedding.sortedLE_listMap, RelEmbedding.orderEmbeddingOfLTEmbedding_apply, univ_option, exteriorPower.pairingDual_apply_apply_eq_one_zero, Subalgebra.coe_toSubmodule, MeasurableSpace.generateMeasurableRec_omega_one, OrderEmbedding.birkhoffSet_apply, Finset.mapEmbedding_apply, PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier, PartOrdEmb.ext_iff, Nat.exists_subseq_of_forall_mem_union, Subalgebra.restrictScalars_toSubmodule, FiniteMulArchimedeanClass.subsemigroup_eq_subgroup, StarAlgebra.adjoin_eq_span, wellQuasiOrdered_iff_exists_monotone_subseq, Set.OrdConnected.apply_covBy_apply_iff, Ordinal.mem_range_preOmega_iff, Submodule.iSup_eq_toSubmodule_range, Ordinal.omega_max, Nat.orderEmbeddingOfSet_range, Set.OrdConnected.apply_wcovBy_apply_iff, OrderEmbedding.sorted_le_listMap, Cardinal.aleph_eq_preAleph, Ordinal.omega_pos, OrderEmbedding.lt_iff_lt, IsIntegral.fg_adjoin_singleton, OrderEmbedding.preimage_Ioi, Composition.boundary_last, WithTop.Ioc_coe_top, Ordinal.toGame_injective, CountableInterFilter.toCardinalInterFilter, Cardinal.aleph_one_eq_lift, OrderEmbedding.isEmbedding_of_ordConnected, Cardinal.aleph_toENat, Cardinal.countable_iff_lt_aleph_one, MvPolynomial.range_mapAlgHom, FormalMultilinearSeries.applyComposition_update, OrderEmbedding.range_inj, IsChain.image_embedding, OrderEmbedding.sortedGT_listMap, OrderEmbedding.coe_subtype, OrderEmbedding.ltEmbedding_apply, MeasurableSpace.generateMeasurableRec_omega1, FiniteDimensional.subalgebra_toSubmodule, Field.Emb.Cardinal.iSup_filtration, Cardinal.aleph_limit, Set.partiallyWellOrderedOn_iff_exists_monotone_subseq, OrderEmbedding.map_inf_le, Ordinal.preOmega_le_preOmega, FirstOrder.Language.LHom.mem_substructureReduct, Ordinal.lift_omega, Ordinal.preOmega_omega0, OrderEmbedding.preimage_Ioo, OrderEmbedding.coe_ofMapLEIff, Cardinal.aleph0_mul_aleph, Ordinal.preOmega_lt_preOmega, Cardinal.lift_lt_aleph1, HahnSeries.support_embDomain_subset, OrderEmbedding.le_iff_le, CompositionAsSet.boundary_length, WithTop.some_mem_insertTop, Subalgebra.pointwise_smul_toSubmodule, Set.powersetCard.mem_range_ofFinEmbEquiv_symm_iff_mem, Cardinal.isSuccLimit_omega, Ordinal.cof_omega, Cardinal.aleph_one_lt_lift, Affine.Simplex.face_points', WithTop.Icc_coe_top, Subalgebra.prod_toSubmodule, BoxIntegral.unitPartition.diam_boxIcc, Finset.orderEmbOfFin_mem, Ordinal.preOmega_natCast, PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier, Composition.coe_embedding, Finset.listMap_orderEmbOfFin_finRange, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, PartOrdEmb.coe_id, Cardinal.mem_range_aleph_iff, Cardinal.aleph_lt_aleph, AlgHom.equalizer_toSubmodule, HahnSeries.orderTop_embDomain, OrderEmbedding.withBotMap_apply, Subalgebra.pi_toSubmodule, WCovBy.image, OrderEmbedding.subtype_injective, OrderEmbedding.sorted_gt_listMap, Composition.mem_range_embedding_iff, finSumEquivOfFinset_inl, OrderEmbedding.image_Ico, Ordinal.IsInitial.mem_range_preOmega, Finset.eraseNone_insertNone, List.sublist_iff_exists_orderEmbedding_getElem?_eq, InitialSeg.coe_toOrderEmbedding, Cardinal.aleph_toNat, Ordinal.range_preOmega, Finset.orderEmbOfFin_compl_singleton_apply, Ordinal.preOmega_max, Ordinal.toGame_nadd, CompositionAsSet.boundary_zero, WithBot.some_mem_insertBot, Subalgebra.rank_toSubmodule, Cardinal.succ_aleph0, Subalgebra.fg_bot_toSubmodule, WithBot.bot_mem_insertBot, WithBot.Icc_bot_coe, Ordinal.toGame_natCast, Fin.coe_succOrderEmb, exists_orderEmbedding_covby_of_forall_covby_finite_of_bot, Ordinal.le_omega_self, Cardinal.aleph_zero, OrderEmbedding.birkhoffFinset_sup, Ordinal.toGame_le_iff, Ordinal.omega_eq_preOmega, Cardinal.lift_lt_aleph_one, Composition.single_embedding, OrderEmbedding.eq_iff_eq, DFinsupp.orderEmbeddingToFun_apply, Finset.mem_insertNone, Ordinal.isNormal_omega, MeasurableSpace.generateMeasurable_eq_rec, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective
|
instFunLikeOrderIso ๐ | CompOp | 608 mathmath: IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, OrderIso.sumAssoc_apply_inl_inl, WithBot.coe_toDualTopEquiv_eq, Submodule.toAddSubgroup_toZModSubmodule, OrderIso.isLUB_image, Submodule.toAddSubmonoid_toNatSubmodule, Ordinal.toNimber_eq_zero, NNReal.orderIsoIccZeroCoe_apply_coe_coe, CategoryTheory.ComposableArrows.opEquivalence_counitIso_inv_app_app, OrderIso.map_radical, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, OrderIso.map_csInf, LowerSet.map_Iio, OrderIso.pnatIsoNat_symm_apply, LowerSet.compl_map, WithTop.toDualBotEquiv_coe, OrderIso.image_Icc, OrderIso.isMin_apply, OrderIso.continuous, OrderIso.map_bot', OrderIso.arrowCongr_apply, WithBot.orderIsoPUnitSumLex_symm_inl, OrderIso.isGLB_preimage', OrderIso.symm_trans_apply, OrderIso.coe_dualDual_symm, WithLp.prod_nndist_eq_of_L2, OrderIso.withTopCongr_apply, mem_subalgebraEquivIntermediateField, OrderIso.lt_iff_lt, finSuccAboveOrderIso_symm_apply_last, OrderIso.isCoatom_iff, IsChain.preimage_iso_iff, OrderIso.toFun_eq_coe, StrictMono.orderIsoOfSurjective_symm_apply_self, WithBot.subtypeOrderIso_symm_apply, Flag.coe_map, IsChain.image_iso, Submonoid.fg_iff_add_fg, Sublattice.map_equiv_eq_comap_symm, OrderIso.sumLexIicIoi_symm_apply_of_lt, OrderIso.tendsto_atTop_iff, OrderIso.range_eq, Ordinal.toNatOrdinal_eq_one, idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, upperClosure_image, AddSubgroup.mem_toSubgroup', coe_factor_orderIso_map_eq_one_iff, HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk, List.SortedLT.coe_getIso_symm_apply, OrderIso.toRelIsoLT_apply, CFC.nnnorm_sqrt, NNReal.sqrt_le_iff_le_sq, OrderIso.isBoundedUnder_ge_comp, OrderIso.map_csInf', OrderIso.monotone, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, OrderIso.image_Ico, OrderIso.invENNReal_symm_apply, pow_image_of_prime_by_factor_orderIso_dvd, SetTheory.PGame.grundyValue_eq_iff_equiv_nim, NNReal.sqrt_mul_lt_half_add_of_ne, OrderIso.isGLB_image', OrderIso.sortedGT_listMap, OrderIso.isNormal, NatOrdinal.toOrdinal_min, SetTheory.PGame.grundyValue_nim_add_nim, Finset.map_truncatedInf, Nimber.succ_def, OrderIso.preimage_Ioc, lowerClosure_image, OrderIso.map_pred, OrderIso.bddAbove_image, Fin.orderIsoTriple_zero, IsChain.preimage_iso, OrderIso.equivalence_functor, OrderIso.isLUB_image', Function.sSup_div_semiconj, Frm.Iso.mk_hom, Tropical.tropOrderIso_symm_coe_fn, WithBot.orderIsoPUnitSumLex_symm_inr, NNReal.agmSequences_zero, MonoidHom.coe_toMultiplicative_range, OrderIso.image_symm_image, OrderIso.essSup_apply, Subspace.dualAnnihilator_dualAnnihilator_eq, UpperSet.mem_map, OrderIso.sumLexIioIci_symm_apply_Ici, OrderIso.dualAntisymmetrization_symm_apply, OrderIso.strictMono, UpperSet.map_map, OrderIso.apply_symm_apply, OrderIso.isGLB_image, AddEquiv.coe_comapAddSubgroup, NNReal.sqrt_sq, EuclideanSpace.nndist_eq, NNReal.sqrt_pos, Cardinal.isNormal_preAleph, OrderIso.sumLexAssoc_symm_apply_inr_inr, StrictMono.orderIsoOfSurjective_self_symm_apply, NNReal.le_sqrt_iff_sq_le, NNReal.sqrt_eq_rpow, Finset.orderIsoOfFin_symm_apply, PiLp.nnnorm_eq_of_L2, Cardinal.preAleph_nat, OrderIso.bijective, CategoryTheory.Equivalence.toOrderIso_apply, Ordinal.toNimber_min, SemilatSupCat.Iso.mk_inv_toFun, NNReal.sqrt_zero, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, Fin.orderIsoSingleton_apply, HeytAlg.Iso.mk_inv, OrderIso.infIrredUpperSet_symm_apply, OrderIso.map_inf, List.SortedLT.coe_getIso_apply, OrderIso.map_csSup_of_directedOn, OrderIso.image_setOf_maximal, OrderIso.refl_apply, LowerSet.coe_map, Nimber.toOrdinal_max, Fin.orderIsoPair_zero, IsAntichain.preimage_iso_iff, Cardinal.preAleph_le_aleph, Module.mapEvalEquiv_apply, IsOrderRightAdjoint.comp_orderIso, Finpartition.parts_map, Nimber.toOrdinal_min, AddSubsemigroup.toSubsemigroup'_closure, OrderIso.comap_atTop, OrderIso.dualDual_apply, Matrix.frobenius_nnnorm_one, NatOrdinal.succ_def, OrderIso.dual_apply, Order.height_orderIso, BddOrd.Iso.mk_hom, StrictMono.coe_orderIsoOfSurjective, OrderIso.sumLexIicIoi_symm_apply_of_le, OrderIso.map_sInf_eq_sInf_symm_preimage, Ordinal.card_le_preAleph, NNReal.strictConcaveOn_sqrt, OrderIso.map_iSup, Submonoid.toAddSubmonoid_closure, NNReal.sqrt_le_sqrt, FiniteMulArchimedeanClass.withTopOrderIso_apply_coe, OrderIso.map_ciInf_of_directed, AddSubmonoid.toNatSubmodule_toAddSubmonoid, OrderIso.supIrredLowerSet_symm_apply, OrderIso.ofRelIsoLT_apply, CircleDeg1Lift.coe_toOrderIso_symm, AddSubmonoid.toNatSubmodule_closure, NumberField.Units.span_basisOfIsMaxRank, PrimeSpectrum.isIdempotentElemEquivClopens_symm_bot, DistLat.Iso.mk_inv, OrderIso.to_galoisConnection, AddSubgroup.toZModSubmodule_toAddSubgroup, OrderIso.isCompl, CategoryTheory.ComposableArrows.opEquivalence_unitIso_inv_app, IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq, Ordinal.toNatOrdinal_min, Cardinal.preAleph_omega0, OrderIso.coe_symm_toEquiv, OrderIso.map_ciSup, OrderIso.coe_dualDual, CircleDeg1Lift.coe_toOrderIso_inv, OrderIso.map_atBot, LinOrd.Iso.mk_hom, Real.coe_expOrderIso_apply, PrimeSpectrum.isIdempotentElemEquivClopens_one_sub, WithTop.orderIsoSumLexPUnit_toLex, OrderIso.preimage_Ioo, Subgroup.fg_iff_add_fg, IsAntichain.image_iso, Module.Basis.addSubgroupOfClosure_repr_apply, Cardinal.le_preAleph_ord, OrderIso.coe_toRelIsoLT, OrderIso.image_Iio, OrderIso.trans_apply, Tuple.graphEquivโ_apply, WithTop.orderIsoSumLexPUnit_symm_inl, Finset.coe_orderIsoOfFin_apply, NNReal.sqrt_eq_iff_eq_sq, NatOrdinal.toOrdinal_max, OrderIso.isGLB_preimage, AddSubgroup.toIntSubmodule_symm, Lat.Iso.mk_inv, OrderIso.map_succ, Complex.antilipschitz_equivRealProd, OrderIso.sumLexIioIci_symm_apply_Iio, mem_subalgebraEquivIntermediateField_symm, AddSubgroup.toSubgroup_closure, WithTop.toDualBotEquiv_symm_top, PrimeSpectrum.isIdempotentElemEquivClopens_symm_inf, OrderIso.coe_toOrderEmbedding, OrderIso.map_sSup_eq_sSup_symm_preimage, List.Sorted.coe_getIso_symm_apply, IsDedekindDomain.primesOverEquivPrimesOver_apply, CategoryTheory.ComposableArrows.opEquivalence_functor_obj_map, OrderIso.sumDualDistrib_symm_inl, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, Real.log_of_pos, OrderIso.bddBelow_preimage, MulEquiv.coe_comapSubgroup, Subgroup.mem_toAddSubgroup', Submodule.mk_mem_projectivization_iff, AddSubmonoid.toSubmonoid_closure, Frm.Iso.mk_inv, ProbabilityTheory.Kernel.HasSubgaussianMGF.add, WithLp.prod_nnnorm_eq_of_L2, ENNReal.orderIsoIicCoe_symm_apply_coe, Ordinal.toNatOrdinal_one, Subsemigroup.toAddSubsemigroup_closure, NonemptyFinLinOrd.Iso.mk_inv, OrderIso.map_iInf, MonoidHom.coe_toAdditive_map, OrderIso.isAtom_iff, Submodule.orderIsoMapComap_apply', OrderIso.conj_apply, Nimber.add_nat, OrderIso.sumAssoc_apply_inr, OrderIso.symm_apply_eq, OrderIso.map_cofinal, Fin.orderIsoTriple_one, Tuple.self_comp_sort, NNReal.sqrt_mul, Submodule.toIntSubmodule_toAddSubgroup, disjoint_map_orderIso_iff, FiniteMulArchimedeanClass.withTopOrderIso_symm_apply, OrderIso.sumLexIicIoi_symm_apply_Iic, OrderIso.arrowCongr_symm_apply, OrderIso.image_Iic, WithTop.orderIsoSumLexPUnit_top, WithTop.subtypeOrderIso_symm_apply, CategoryTheory.ComposableArrows.opEquivalence_inverse_obj, OrderIso.preimage_Iio, NNReal.sqrt_eq_zero, MulEquiv.coe_mapSubgroup, OrderIso.le_iff_le, NNReal.mul_self_sqrt, Prod.Lex.uniqueProd_apply, OrderIso.map_csSup', OrderIso.image_setOf_minimal, Real.sinOrderIso_apply, OrderIso.supIrredLowerSet_apply, WithBot.toDualTopEquiv_coe, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, Cardinal.preAleph_limit, OrderIso.symm_preimage_preimage, IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq, UpperSet.map_Ici, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, OrderIso.tendsto_atTop, Submodule.toAddSubgroup_toIntSubmodule, OrderIso.sumLexIicIoi_symm_apply_Ioi, CategoryTheory.ComposableArrows.opEquivalence_unitIso_hom_app, RingEquiv.mapTwoSidedIdeal_apply, OrderIso.lt_symm_apply, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_snd, OrderIso.toInitialSeg_toFun, AddSubgroup.toZModSubmodule_symm, NNReal.agm_eq_agm_gm_am, OrderIso.surjective, Ideal.idealProdEquiv_symm_apply, NNReal.le_gm_and_am_le, Submodule.orderIsoMapComap_symm_apply', NNReal.continuous_sqrt, NatOrdinal.toOrdinal_natCast, RingEquiv.idealComapOrderIso_symm_apply, Codisjoint.map_orderIso, SetTheory.PGame.equiv_nim_grundyValue, OrderIso.coe_prodComm, PrimeSpectrum.isIdempotentElemEquivClopens_symm_sup, AddSubmonoid.toNatSubmodule_symm, IsAntichain.preimage_iso, OrderIso.image_Ici, OrderIso.coe_refl, List.Sorted.coe_getIso_apply, Ordinal.toNimber_one, Cardinal.ord_preAleph, OrderIso.equivalence_counitIso, OrderIso.map_csInf_of_directedOn, OrderIso.dualAntisymmetrization_apply, Fintype.coe_finsetOrderIsoSet_symm, Nat.Subtype.orderIsoOfNat_apply, Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat, OrderIso.sumAssoc_symm_apply_inr_inl, OrderIso.sumLexIicIoi_apply_inr, Multiplicative.mem_toSubgroup, Cardinal.preAleph_max, OrderIso.map_ciSup', OrderIso.preimage_Icc, NNReal.sqrt_eq_one, LowerSet.mem_map, NNReal.sqrt_pos_of_pos, Nimber.toOrdinal_eq_one, OrderIso.comap_atBot, Fin.coe_orderIso_apply, Submodule.orderIsoMapComap_symm_apply, Subgroup.toAddSubgroup_closure, AddEquiv.coe_mapAddSubgroup, OrderIso.withBotCongr_apply, CircleDeg1Lift.coe_toOrderIso, AddSubgroup.coe_toZModSubmodule, finSuccAboveOrderIso_apply, WithBot.toDualTopEquiv_symm_bot, OrderHom.curry_apply, Nat.nth_apply_eq_orderIsoOfNat, Cardinal.preAleph_le_of_isSuccPrelimit, Cardinal.aleph0_le_preAleph, Cardinal.preAleph_succ, ENNReal.orderIsoUnitIntervalBirational_apply_coe, OrderIso.coe_symm_toRelIsoGT, Nimber.toOrdinal_one, IsGalois.intermediateFieldEquivSubgroup_symm_apply, OrderIso.sumLexAssoc_symm_apply_inr_inl, Finsupp.coe_orderIsoMultiset_symm, OrderIso.bddAbove_preimage, NNReal.sum_mul_le_sqrt_mul_sqrt, OrderIso.sumLexAssoc_apply_inl_inl, emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso, HahnSeries.archimedeanClassOrderIsoWithTop_apply, Finset.map_truncatedSup, Submodule.mem_projectivization_iff_submodule_le, Fintype.coe_finsetOrderIsoSet, Preord.Iso.mk_hom, emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso, Subgroup.index_toAddSubgroup, AddMonoidHom.coe_toIntLinearMap_ker, OrderIso.infIrredUpperSet_apply, NNReal.one_le_sqrt, OrderIso.sumLexEmpty_apply_inl, WithBot.toDualTopEquiv_symm_coe, OrderIso.sumLexIicIoi_apply_inl, OrderIso.sumDualDistrib_inl, OrderIso.image_Ioi, Module.AEval.mem_mapSubmodule_symm_apply, Sublattice.comap_equiv_eq_map_symm, OrderIso.isLUB_preimage, Antisymmetrization.prodEquiv_symm_apply_mk, OrderIso.apply_eq_iff_eq_symm_apply, AddSubgroup.coe_toIntSubmodule, SemilatInfCat.Iso.mk_inv_toFun, OrderIso.injective, PrimeSpectrum.isIdempotentElemEquivClopens_apply_toOpens, PrimeSpectrum.basicOpen_isIdempotentElemEquivClopens_symm, LinOrd.Iso.mk_inv, BddOrd.Iso.mk_inv, ProbabilityTheory.HasSubgaussianMGF.add, Cardinal.preAleph_zero, MonoidHom.coe_toAdditive_range, OrderIso.upperBounds_image, OrderIso.coe_toRelIsoGT, OrderIso.sumDualDistrib_symm_inr, NNReal.orderIsoIccZeroCoe_symm_apply_coe, OrderIso.preimage_Ici, SemilatSupCat.Iso.mk_hom_toFun, Ordinal.toNatOrdinal_zero, Real.coe_comp_expOrderIso, Fin.revOrderIso_symm_apply, NatOrdinal.toOrdinal_eq_zero, CompleteLat.Iso.mk_hom, OrderIso.essInf_apply, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, hahnEmbedding_isOrderedModule_rat, WithBot.orderIsoPUnitSumLex_toLex, AddSubgroup.MapSubtype.orderIso_symm_apply, Cardinal.preAleph_le_preAleph, OrderIso.coe_symm_toRelIsoLT, OrderIso.sortedLT_listMap, AddMonoidHom.coe_toIntLinearMap_map, OrderIso.symm_apply_le, OrderIso.map_top, FiniteArchimedeanClass.withTopOrderIso_symm_apply, WithTop.toDualBotEquiv_symm_coe, Ordinal.toNatOrdinal_eq_zero, OrderIso.apply_eq_iff_eq, OrderIso.emptySumLex_apply_inr, idealFactorsEquivOfQuotEquiv_is_dvd_iso, Submodule.coe_mapIic_apply, AddMonoidHom.coe_toIntLinearMap_range, Cardinal.preAleph_lt_preAleph, WithBot.subtypeOrderIso_apply_coe, OrderIso.equivalence_inverse, AddMonoidHom.coe_toMultiplicative_map, OrderIso.sumLexDualAntidistrib_symm_inl, OrderIso.map_sup, OrderIso.map_ciSup_set, OrderIso.lowerBounds_image, FinPartOrd.Iso.mk_inv, DivisibleHull.archimedeanClassOrderIso_apply, UpperSet.map_Ioi, OrderIso.image_Ioc, Subgroup.toAddSubgroup_comap, OrderIso.isBoundedUnder_le_comp, OrderIso.tendsto_atBot_iff, OrderIso.map_ciInf, OrderIso.preimage_Ioi, Equiv.coe_toOrderIso, OrderIso.leftOrdContinuous, codisjoint_map_orderIso_iff, WithBot.toDualTopEquiv_bot, PartOrd.Iso.mk_hom, PrimeSpectrum.isIdempotentElemEquivClopens_symm_top, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', IsAntichain.image_iso_iff, nucleusIsoSublocale.eq_toSublocale, OrderIso.le_symm_apply, OrderIso.ofHomInv_symm_apply, Submodule.AddMonoidHom.coe_toIntLinearMap_comap, OrderIso.symm_apply_lt, OrderIso.sumLexIioIci_symm_apply_of_ge, CFC.sqrt_eq_cfc, Ordinal.card_preOmega, orderIsoShrink_apply, CategoryTheory.ComposableArrows.opEquivalence_inverse_map, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, OrderIso.isMax_apply, SemilatInfCat.Iso.mk_hom_toFun, IsDedekindDomain.primesOverEquivPrimesOver_symm_apply, FiniteArchimedeanClass.coe_congrOrderIso_apply, Ordinal.toNatOrdinal_natCast, OrderHom.curry_symm_apply, IsUpperSet.image, iSupIndep_map_orderIso_iff, NatOrdinal.toOrdinal_one, OrderIso.sumAssoc_symm_apply_inr_inr, OrderIso.rightOrdContinuous, Ordinal.toNimber_zero, orderIsoShrink_symm_apply, nucleusIsoSublocale.symm_eq_toNucleus, NatOrdinal.toOrdinal_toNatOrdinal, AddSubmonoid.coe_toNatSubmodule, OrderIso.preimage_symm_preimage, OrderIso.map_iInfโ, OrderIso.map_csSup, OrderIso.map_sSup, NNReal.sqrt_one, UpperSet.compl_map, AddSubgroup.fg_iff_mul_fg, Cardinal.preAleph_le_of_strictMono, CFC.sqrt_algebraMap, OrderIso.coe_trans, Cardinal.preAleph_le_preBeth, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, OrderEmbedding.birkhoffSet_apply, WithTop.subtypeOrderIso_apply_coe, NNReal.sqrt_le_one, AddSubgroup.toIntSubmodule_toAddSubgroup, EReal.expOrderIso_apply, HahnSeries.finiteArchimedeanClassOrderIsoLex_apply_fst, Cardinal.preAleph_pos, DivisibleHull.archimedeanClassOrderIso_symm_apply, OrderIso.sumLexIioIci_apply_inl, OrderIso.map_ciSup_of_directed, WithTop.orderIsoSumLexPUnit_symm_inr, AddSubgroup.toSubgroup'_closure, IsChain.image_iso_iff, UpperSet.coe_map, Preord.Iso.mk_inv, OrderIso.sumDualDistrib_inr, Disjoint.map_orderIso, OrderIso.symm_apply_apply, Ordinal.toNimber_toOrdinal, OrderIso.apply_blimsup, PartOrd.Iso.mk_inv, Ordinal.toNimber_max, Submonoid.toAddSubmonoid'_closure, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, OrderIso.sumLexAssoc_apply_inr, LowerSet.map_Iic, OrderIso.funUnique_symm_apply, OrderIso.map_ciSup_set_of_directedOn, DistLat.Iso.mk_hom, factor_orderIso_map_one_eq_bot, OrderIso.image_eq_preimage_symm, AddSubsemigroup.toSubsemigroup_closure, OrderIso.preimage_image, HeytAlg.Iso.mk_hom, OrderIso.map_ciInf_set_of_directedOn, Ordinal.toNimber_eq_one, Cardinal.aleph_eq_preAleph, BooleanSubalgebra.mem_map_equiv, Sublattice.map_symm_eq_iff_eq_map, Lat.Iso.mk_hom, OrderIso.sumAssoc_apply_inl_inr, OrderIso.map_sInf, NNReal.sqrt_div, Antisymmetrization.prodEquiv_apply_mk, Subgroup.toAddSubgroup'_closure, HahnSeries.finiteArchimedeanClassOrderIso_apply, OrderIso.map_iSupโ, EuclideanSpace.nnnorm_eq, AddSubgroup.relIndex_eq_natAbs_det, OrderIso.map_top', OrderIso.bddBelow_image, Prod.Lex.prodUnique_apply, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, CategoryTheory.Equivalence.toOrderIso_symm_apply, NNReal.agmSequences_succ', OrderIso.image_Ioo, AddSubgroup.index_toSubgroup, Real.coe_sqrt, SetTheory.PGame.nim_grundyValue, map_prime_of_factor_orderIso, AddSubgroup.toIntSubmodule_closure, OrderIso.symm_image_image, AddSubgroup.mem_toZModSubmodule, NNReal.sum_sqrt_mul_sqrt_le, Fin.orderIsoTriple_two, OrderIso.coe_toHomeomorph, OrderIso.map_ciInf_set, iSupIndep.map_orderIso, NNReal.sqrt_mul_le_half_add, OrderIso.toCompleteLatticeHom_toFun, OrderIso.sumAssoc_symm_apply_inl, Nimber.toOrdinal_zero, NatOrdinal.toOrdinal_zero, OrderIso.isLUB_preimage', Nat.nth_eq_orderIsoOfNat, OrderIso.image_preimage, OrderIso.tendsto_atBot, Nimber.toOrdinal_toNimber, CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app, OrderIso.sumLexDualAntidistrib_symm_inr, Ordinal.toNatOrdinal_toOrdinal, OrderIso.map_bot, OrderIso.sumLexDualAntidistrib_inr, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, FinPartOrd.Iso.mk_hom, NatOrdinal.toOrdinal_eq_one, PrimeSpectrum.isIdempotentElemEquivClopens_mul, mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors, NNReal.sqrt_mul_self, Real.log_of_ne_zero, OrderIso.map_csSup_of_directedOn', Module.AEval.mem_mapSubmodule_apply, Subsemigroup.toAddSubsemigroup'_closure, Ordinal.nmul_eq_mul, OrderIso.dual_symm_apply, NNReal.sqrt_inv, AddSubgroup.toSubgroup_comap, OrderIso.coe_toEquiv, OrderIso.sumLexDualAntidistrib_inl, PrimeSpectrum.coe_isIdempotentElemEquivClopens_apply, OrderIso.coe_toHomeomorph_symm, OrderIso.sumLexAssoc_symm_apply_inl, NNReal.dist_gm_am_le, OrderIso.preimage_Ico, OrderIso.equivalence_unitIso, PrimeSpectrum.isIdempotentElemEquivClopens_symm_compl, Finset.sumEquiv_symm_apply, Sublattice.mem_map_equiv, ENNReal.logOrderIso_apply, Order.coheight_orderIso, OrderIso.sumLexIioIci_apply_inr, LowerSet.map_map, Module.Basis.addSubgroupOfClosure_apply, CompleteLat.Iso.mk_inv, OrderIso.sumLexIioIci_symm_apply_of_lt, FiniteArchimedeanClass.withTopOrderIso_apply_coe, AddSubmonoid.fg_iff_mul_fg, NNReal.agmSequences_succ, OrderIso.toRelIsoGT_apply, ENNReal.orderIsoIicOneBirational_symm_apply, Tropical.tropOrderIso_coe_fn, FiniteMulArchimedeanClass.coe_congrOrderIso_apply, Tactic.NormNum.isNat_nnrealSqrt, SetTheory.PGame.nim_add_nim_equiv, OrderIso.sumLexAssoc_apply_inl_inr, OrderIso.map_csInf_of_directedOn', Finsupp.coe_orderIsoMultiset, AddSubmonoid.toSubmonoid'_closure, NNReal.sqrt_lt_sqrt, MonoidHom.coe_toAdditive_ker, PiLp.nndist_eq_of_L2, Projectivization.Subspace.mem_submodule_iff, WithTop.coe_toDualBotEquiv, Ordinal.toNatOrdinal_max, NonemptyFinLinOrd.Iso.mk_hom, Nimber.toOrdinal_eq_zero, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual, OrderRingIso.coe_toOrderIso, Additive.mem_toAddSubgroup, Fin.orderIsoPair_one, OrderIso.ext_iff, WithTop.toDualBotEquiv_top, OrderIso.map_atTop, hahnEmbedding_isOrderedAddMonoid, NNReal.sq_sqrt, Cardinal.lift_preAleph, OrderIso.isCompl_iff, Real.coe_sinOrderIso_apply, Subgroup.relIndex_toAddSubgroup, Module.mapEvalEquiv_symm_apply, IsOrderRightAdjoint.orderIso_comp, MonoidHom.coe_toMultiplicative_ker, WithBot.orderIsoPUnitSumLex_bot, OrderIso.apply_bliminf, IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, OrderIso.map_minimal_mem, OrderIso.dualDual_symm_apply, IsLowerSet.image, Ordinal.nadd_eq_add, hahnEmbedding_isOrderedModule, OrderIso.preimage_Iic, Cardinal.isRegular_preAleph_succ, OrderIso.map_maximal_mem, Subgroup.MapSubtype.orderIso_symm_apply, AddSubgroup.relIndex_toSubgroup
|
ยซterm_โo_ยป ๐ | CompOp | โ |
ยซterm_โชo_ยป ๐ | CompOp | โ |
ยซterm_โo_ยป ๐ | CompOp | โ |