| Metric | Count |
|---|
DefinitionsgciOrdCard, ord, orderEmbedding, toTypeOrderBot, univ, ToType, mk, toOrd, add, addMonoidWithOne, card, enum, enumIsoToType, inhabited, initialSegToType, instCoeOutToType, instCoeToTypeElemIio, instConditionallyCompleteLinearOrderBot, instLinearOrder, instOrderBot, instSuccAddOrder, instSuccOrder, instSuccOrderToType, isEquivalent, liftInitialSeg, liftOnWellOrder, liftPrincipalSeg, omega0, one, partialOrder, principalSegToType, termTypeLT_, termฯ, toType, toTypeOrderBot, type, typein, uniqueIioOne, uniqueToTypeOne, univ, wellFoundedRelation, zero, WellOrder, inhabited, r, ฮฑ, hasWellFounded_toType, linearOrder_toType | 48 |
Theoremsuniv, aleph0_lt_univ, bddAbove_ord_image_iff, card_le_iff, card_le_of_le_ord, card_ord, card_surjective, card_typein_lt, card_typein_toType_lt, gc_ord_card, isNormal_ord, lift_lt_univ, lift_lt_univ', lift_ord, lift_univ, lt_ord, lt_ord_succ_card, lt_univ, lt_univ', mk_Iio_ord_toType, mk_ord_toType, mk_toType, nat_lt_univ, omega0_le_ord, omega0_lt_ord, orderEmbedding_coe, ord_aleph0, ord_card_le, ord_eq, ord_eq_Inf, ord_eq_omega0, ord_eq_one, ord_eq_zero, ord_inj, ord_injective, ord_le, ord_le_omega0, ord_le_ord, ord_le_type, ord_lt_omega0, ord_lt_ord, ord_mono, ord_nat, ord_ofNat, ord_one, ord_strictMono, ord_univ, ord_zero, small_iff_lift_mk_lt_univ, univ_id, univ_ne_zero, univ_pos, univ_umax, ordinal_type_le, lt_ord_of_lt, lt_ord_of_lt, Iio_one_default_eq, mk_apply, mk_symm_apply_coe, add_one_eq_succ, add_succ, aleph0_le_card, bot_eq_zero, canonicallyOrderedAdd, card_add, card_eq_nat, card_eq_ofNat, card_eq_one, card_eq_zero, card_le_card, card_le_nat, card_le_ofNat, card_le_one, card_lt_aleph0, card_lt_nat, card_lt_ofNat, card_nat, card_ofNat, card_omega0, card_one, card_succ, card_type, card_typein, card_univ, card_zero, enum_inj, enum_le_enum, enum_le_enum', enum_lt_enum, enum_symm_apply_coe, enum_type, enum_typein, enum_zero_eq_bot, enum_zero_le, enum_zero_le', eq_zero_or_pos, existsAddOfLE, induction, inductionOn, inductionOnWellOrder, inductionOnโ, inductionOnโ, instAddLeftMono, instAddRightMono, instIsEmptyIioZero, instNeZeroOne, instNoMaxOrder, instZeroLEOneClass, isEmpty_toType_zero, le_add_left, le_add_right, le_enum_succ, le_lift_iff, le_one_iff, le_zero, liftInitialSeg_coe, liftOnWellOrder_type, liftPrincipalSeg_coe, liftPrincipalSeg_top, liftPrincipalSeg_top', lift_card, lift_id, lift_id', lift_inj, lift_le, lift_lift, lift_lt, lift_omega0, lift_one, lift_type_eq, lift_type_le, lift_type_lt, lift_typein_top, lift_umax, lift_univ, lift_uzero, lift_zero, lt_lift_iff, lt_one_iff_zero, lt_wf, max_eq_zero, max_zero_left, max_zero_right, mem_range_lift_of_card_le, mem_range_lift_of_le, mem_range_typein_iff, natCast_succ, nat_le_card, nat_lt_card, nontrivial, not_lt_zero, ofNat_le_card, ofNat_lt_card, one_le_card, one_le_iff_ne_zero, one_lt_card, one_ne_zero, one_toType_eq, relIso_enum, relIso_enum', sInf_empty, small_Icc, small_Ico, small_Iic, small_Iio, small_Ioc, small_Ioo, succ_ne_zero, succ_one, succ_pos, succ_zero, toType_empty_iff_eq_zero, toType_nonempty_iff_ne_zero, top_typein, type_empty, type_eq, type_eq_one_iff_unique, type_eq_one_of_unique, type_eq_zero_iff_isEmpty, type_eq_zero_of_empty, type_fin, type_fintype, type_le_iff, type_le_iff', type_lift_preimage, type_lt_iff, type_nat_lt, type_ne_zero_iff_nonempty, type_ne_zero_of_nonempty, type_pEmpty, type_pUnit, type_preimage, type_subrel, type_sum_lex, type_toType, type_uLift, type_unit, typein_apply, typein_enum, typein_inj, typein_injective, typein_le_typein, typein_le_typein', typein_lt_self, typein_lt_type, typein_lt_typein, typein_one_toType, typein_surj, typein_surjOn, typein_top, univ_id, univ_umax, wellFoundedLT, zero_lt_card, ordinal_type_lt, ordinal_type_le, ordinal_lift_type_eq, ordinal_type_eq, wo, wellFoundedLT_toType | 220 |
| Total | 268 |
| Name | Category | Theorems |
|---|
ToType ๐ | CompOp | 81 mathmath: iSup_eq_bsup, iSup_typein_succ, Field.Emb.Cardinal.directed_filtration, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, Field.Emb.Cardinal.filtration_succ, card_iSup_Iio_le_sum_card, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, Field.Emb.Cardinal.two_le_deg, Field.Emb.Cardinal.isLeast_leastExt, enum_le_enum', Field.Emb.Cardinal.succEquiv_coherence, Cardinal.noMaxOrder, CategoryTheory.OrthogonalReflection.iteration_map_succ, CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily, Field.Emb.Cardinal.noMaxOrder_rank_toType, toType_noMax_of_succ_lt, toType_nonempty_iff_ne_zero, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, CategoryTheory.instIsCardinalFilteredToTypeOrd, CategoryTheory.SmallCategoryCardinalLT.hasCardinalLT, Field.Emb.Cardinal.strictMono_leastExt, CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasIterationOfShape, sup_eq_bsup, Field.Emb.Cardinal.equivSucc_coherence, CategoryTheory.SmallObject.ฮนFunctorObj_eq, le_enum_succ, Cardinal.card_typein_toType_lt, CategoryTheory.SmallObject.instIsIsoRightAppArrowMapToTypeOrdFunctorIterationFunctor, cof_eq_cof_toType, CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc, comp_familyOfBFamily, SetTheory.PGame.rightMoves_nim, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, ToType.mk_symm_apply_coe, Field.Emb.Cardinal.filtration_apply, enum_succ_eq_top, SetTheory.PGame.leftMoves_nim, iSup_typein_limit, Field.Emb.Cardinal.deg_lt_aleph0, toPGame_leftMoves, range_familyOfBFamily, CategoryTheory.SmallObject.hasIterationOfShape, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, CategoryTheory.SmallObject.ฯFunctorObj_eq, CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument', Cardinal.mk_ord_toType, Field.Emb.Cardinal.strictMono_filtration, lsub_typein, enum_zero_eq_bot, isEmpty_toType_zero, Cardinal.mk_toType, typein_lt_self, Field.Emb.Cardinal.iSup_adjoin_eq_top, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ฮนIteration_app_right, CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropฮนIteration_F, ToType.mk_apply, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument', Field.Emb.Cardinal.adjoin_image_leastExt, typein_one_toType, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, CategoryTheory.SmallCategoryCardinalLT.exists_equivalence, sup_typein_limit, CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit, toType_empty_iff_eq_zero, typein_le_typein', CategoryTheory.SmallObject.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ฮนObj, CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity, type_toPSet, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, Field.Emb.Cardinal.adjoin_basis_eq_top, lsub_eq_blsub, CategoryTheory.SmallObject.preservesColimit, enum_zero_le', CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ฮนIteration_app_right_assoc, familyOfBFamily_enum, type_toType, wellFoundedLT_toType, Cardinal.mk_Iio_ord_toType, sup_typein_succ, one_toType_eq
|
add ๐ | CompOp | 106 mathmath: principal_add_omega, add_absorp, add_succ, dvd_add_iff, add_right_cancel, existsAddOfLE, ONote.nf_repr_split', deriv_add_eq_mul_omega0_add, instAddRightMono, add_le_iff_of_isSuccLimit, principal_add_of_le_one, CNF_foldr, Nimber.succ_def, principal_add_ord, lt_mul_div_add, add_log_le_log_mul, nmul_add_one, le_add_left, opow_add, div_add_mod, mul_add_div, isSuccLimit_add_iff_of_isSuccLimit, nfp_mul_opow_omega0_add, one_add_ofNat, nat_nadd, opow_mul_add_pos, NONote.repr_add, NatOrdinal.succ_def, one_add_omega0, iSup_add_nat, isSuccLimit_add_iff, principal_add_iff_add_left_eq_self, one_add_of_omega0_le, ONote.oadd_mul_nfBelow, log_opow_mul, opow_one_add, lt_sub, opow_mul_add_lt_opow, OrdinalApprox.gfpApprox_add_one, le_sub_of_le, cof_add, lt_add_iff, ONote.repr_add, lt_add_iff_of_isSuccLimit, iSup_add_natCast, add_sub_cancel, sub_lt_of_le, card_add, add_eq_zero_iff, mul_succ, instAddLeftReflectLT, opow_mul_add_lt_opow_mul, sub_le, instAddLeftStrictMono, principal_add_iff_zero_or_omega0_opow, OrdinalApprox.lfpApprox_add_one, principal_add_iff_add_lt_ne_self, principal_add_of_principal_mul, natCast_add_of_omega0_le, one_add_natCast, ONote.repr_opow_auxโ, log_opow_mul_add, lift_add, add_eq_right_iff_mul_omega0_le, mul_add_div_mul, ONote.split_add_lt, add_le_nadd, nfp_add_eq_mul_omega0, mul_add_mod_self, opow_mul_add_lt_opow_succ, leftDistribClass, CNF.foldr, principal_add_one, nadd_nat, principal_add_omega0, isSuccLimit_add, instAddLeftReflectLE, add_omega0, add_sub_cancel_of_le, type_sum_lex, IsInitial.principal_add, Cardinal.beth_eq_preBeth, add_omega0_opow, principal_add_of_principal_mul_opow, mul_add_mod_mul, add_sub_add_cancel, canonicallyOrderedAdd, Cardinal.aleph_eq_preAleph, le_add_right, add_le_iff, isNormal_add_right, principal_add_omega0_opow, instAddLeftMono, add_one_eq_succ, add_le_add_iff_right, opow_mul_add_lt_opow_mul_succ, nfp_add_zero, add_le_right_iff_mul_omega0_le, instAddRightReflectLT, ONote.nf_repr_split, instIsLeftCancelAdd, natCast_add_omega0, sub_sub, le_add_sub, add_one_nmul, omega_eq_preOmega
|
addMonoidWithOne ๐ | CompOp | 78 mathmath: lt_omega0_opow_succ, ONote.repr_one, card_le_ofNat, add_right_cancel, ONote.nf_repr_split', succ_one, SetTheory.Game.birthday_natCast, Cardinal.preAleph_nat, one_add_ofNat, nat_nadd, natCast_mul_omega0, natCast_sub, iSup_add_nat, nat_le_card, natCast_opow, smul_eq_mul, eq_nat_or_omega0_le, nat_lt_card, iSup_mul_nat, natCast_mod, omega0_le, iSup_add_natCast, Nimber.add_nat, card_lt_nat, preOmega_ofNat, Cardinal.ord_ofNat, natCast_add_of_omega0_le, one_add_natCast, NatOrdinal.toOrdinal_natCast, ONote.repr_opow_auxโ, iSup_mul_natCast, lift_natCast, natCast_pow, natCast_mul, natCast_succ, ONote.split_add_lt, natCast_opow_omega0, card_le_nat, type_fintype, toPGame_natCast, SetTheory.PGame.birthday_half, lt_omega0_opow, Cardinal.ord_nat, ofNat_lt_card, ofNat_le_card, card_eq_nat, principal_mul_two, opow_natCast, SetTheory.Game.birthday_ofNat, nadd_nat, isInitial_natCast, natCast_mod_omega0, IsNormal.apply_omega0, omega0_opow_mul_nat_lt, nat_lt_omega0, toNatOrdinal_natCast, card_nat, ONote.repr_ofNat, SetTheory.PGame.birthday_natCast, lt_omega0, add_le_add_iff_right, card_lt_ofNat, iSup_natCast, lift_ofNat, natCast_lt_epsilon, apply_omega0_of_isNormal, preOmega_natCast, ONote.nf_repr_split, Cardinal.preBeth_nat, natCast_lt_of_isSuccLimit, natCast_add_omega0, natCast_lt_gamma, toGame_natCast, type_fin, principal_mul_iff_le_two_or_omega0_opow_opow, instCharZero, natCast_div, card_eq_ofNat
|
card ๐ | CompOp | 77 mathmath: Cardinal.lt_ord_succ_card, lift_card_iSup_le_sum_card, cof_blsub_le, card_le_ofNat, isInitialIso_apply, card_le_aleph, card_iSup_Iio_le_sum_card, card_one, card_zero, card_omega0, card_le_card, card_sInf_range_compl_le_lift, cof_blsub_le_lift, card_le_preAleph, card_omega0_opow, card_sInf_range_compl_le, Cardinal.card_le_iff, nat_le_card, Cardinal.lt_omega_iff_card_lt, card_le_one, IsInitial.card_lt_card, nat_lt_card, IsInitial.ord_card, card_eq_zero, cof_le_card, card_toZFSet, le_cof_iff_blsub, card_le_preBeth, card_iSup_Iio_le_card_mul_iSup, card_lt_nat, one_lt_card, Cardinal.ord_le, card_ofNat, card_add, Cardinal.card_typein_lt, Cardinal.card_typein_toType_lt, card_opow_le_of_omega0_le_right, card_opow_omega0, aleph0_le_card, mk_Iio_ordinal, card_le_nat, ofNat_lt_card, Cardinal.gc_ord_card, card_le_beth, card_succ, card_omega, card_typein, ofNat_le_card, card_opow_eq_of_omega0_le_right, card_type, zero_lt_card, IsInitial.card_le_card, card_eq_nat, card_eq_one, lift_card_sInf_compl_le, Cardinal.card_ord, card_mul, Cardinal.mk_toType, card_opow_le_of_omega0_le_left, card_opow_eq_of_omega0_le_left, card_preOmega, Cardinal.card_surjective, card_nat, card_le_card_vonNeumann, Cardinal.card_le_of_le_ord, card_lt_aleph0, cof_bsup_le_lift, card_lt_ofNat, Cardinal.ord_card_le, lift_card, card_univ, card_opow_le, cof_bsup_le, Cardinal.lt_ord, one_le_card, card_iSup_le_sum_card, card_eq_ofNat
|
enum ๐ | CompOp | 19 mathmath: enum_symm_apply_coe, enum_zero_le, enum_lt_enum, enum_le_enum', le_enum_succ, enum_typein, typein_enum, enum_succ_eq_top, enum_le_enum, enum_zero_eq_bot, relIso_enum', ToType.mk_apply, enum_inj, familyOfBFamily'_enum, enum_zero_le', familyOfBFamily_enum, relIso_enum, enum_type, one_toType_eq
|
enumIsoToType ๐ | CompOp | โ |
inhabited ๐ | CompOp | โ |
initialSegToType ๐ | CompOp | โ |
instCoeOutToType ๐ | CompOp | โ |
instCoeToTypeElemIio ๐ | CompOp | โ |
instConditionallyCompleteLinearOrderBot ๐ | CompOp | 113 mathmath: iSup_eq_iSup, iSup_eq_bsup, lift_card_iSup_le_sum_card, Acc.rank_eq, iSup_pow_natCast, sup_eq_lsub_iff_lt_sup, sInf_compl_lt_lift_ord_succ, max_zero_left, sup_eq_lsub_iff_succ, iSup_typein_succ, log_def, sup_succ_le_lsub, iSup_le_lsub, card_iSup_Iio_le_sum_card, NatOrdinal.toOrdinal_min, toNimber_min, card_sInf_range_compl_le_lift, Nimber.toOrdinal_max, iSup_le, Principal.sSup, Nimber.toOrdinal_min, iSup_pow, deriv_limit, card_sInf_range_compl_le, sSup_eq_bsup, Cardinal.aleph_add_aleph, iSup_add_nat, toNatOrdinal_min, iSup_sum, PSet.rank_insert, iSup_eq_lsub_or_succ_iSup_eq_lsub, sup_succ_eq_lsub, succ_log_def, sSup_ord, NatOrdinal.toOrdinal_max, enumOrd_zero, iSup_mul_nat, sup_le_lsub, iSup_add_natCast, IsNormal.map_iSup, card_iSup_Iio_le_card_mul_iSup, sup_eq_bsup, Principal.iSup, Cardinal.ord_eq_Inf, opow_limit, max_eq_zero, bsup_eq_sup, iSup_mul_natCast, mem_closure_iff_iSup, iSup_lt_ord_lift, Cardinal.aleph_max, Cardinal.preAleph_max, mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, iSup'_eq_bsup, iSup_sequence_lt_omega_one, SetTheory.PGame.birthday_def, IsWellFounded.rank_eq, iSup_typein_limit, derivFamily_limit, ZFSet.rank_range, iSup_ord, ZFSet.rank_insert, sup_eq_sup, le_iSup, iSup_eq_zero_iff, sup_eq_bsup', succ_iSup_eq_lsub_iff, sup_eq_lsub, lift_card_sInf_compl_le, iSup_eq_lsub_iff_lt_iSup, IsNormal.map_iSup_of_bddAbove, lt_iSup_iff, Cardinal.aleph_mul_aleph, IsNormal.map_sSup_of_bddAbove, bsup'_eq_iSup, IsNormal.apply_omega0, iSup_Iio_eq_bsup, iSup_eq_of_range_eq, ZFSet.rank_iUnion, IsNormal.map_sSup, iSup_sequence_lt_omega1, bsup_eq_iSup, lsub_le_succ_iSup, mem_iff_iSup_of_isClosed, sInf_compl_lt_ord_succ, isClosed_iff_iSup, bsup_eq_sup', toNimber_max, sup_typein_limit, omega_max, sup_eq_lsub_or_sup_succ_eq_lsub, ZFSet.rank_pair, iSup_le_iff, Cardinal.iSup_lt_ord_of_isRegular, iSup_eq_lsub, max_zero_right, iSup_eq_lsub_iff, iSup_natCast, iSup_iterate_eq_nfp, apply_omega0_of_isNormal, lsub_le_sup_succ, succ_iSup_le_lsub_iff, IsNormal.apply_of_isSuccLimit, lsub_sum, iSup_lt_ord, ZFSet.rank_union, preOmega_max, card_iSup_le_sum_card, toNatOrdinal_max, PSet.rank_pair, sInf_empty, sup_typein_succ
|
instLinearOrder ๐ | CompOp | 61 mathmath: Profinite.NobelingProof.GoodProducts.sum_to_range, isNormal_mul_right, Profinite.NobelingProof.injective_ฯs', Profinite.NobelingProof.coe_ฯs, liftPrincipalSeg_top', Profinite.NobelingProof.Products.limitOrdinal, Profinite.NobelingProof.Products.eval_ฯs, Cardinal.isNormal_preAleph, Profinite.NobelingProof.Products.eval_ฯs', Profinite.NobelingProof.GoodProducts.span_sum, Profinite.NobelingProof.succ_exact, Profinite.NobelingProof.GoodProducts.smaller_factorization, Profinite.NobelingProof.ฯs'_apply_apply, isNormal_veblen, isNormal_iff_lt_succ_and_bsup_eq, Profinite.NobelingProof.contained_eq_proj, Profinite.NobelingProof.GoodProducts.injective_sum_to, Profinite.NobelingProof.GoodProducts.good_lt_maxProducts, Profinite.NobelingProof.GoodProducts.union_succ, Profinite.NobelingProof.Products.eval_ฯs_image', isNormal_preOmega, isNormal_opow, isNormal_deriv, Cardinal.isNormal_aleph, cmp_veblen, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, isNormal_enumOrd, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, isNormal_iff_lt_succ_and_blsub_eq, CategoryTheory.ObjectProperty.isoClosure_strictLimitsClosureIter_eq_limitsClosure, isNormal_veblen_zero, Profinite.NobelingProof.C0_projOrd, Profinite.NobelingProof.C1_projOrd, Profinite.NobelingProof.ฯs_apply_apply, isNormal_derivFamily, Profinite.NobelingProof.GoodProducts.square_commutes, isNormal_gamma, Profinite.NobelingProof.contained_C1, Profinite.NobelingProof.isClosed_proj, typein_ordinal, Profinite.NobelingProof.swapTrue_mem_C1, univ_id, Profinite.NobelingProof.contained_proj, CategoryTheory.ObjectProperty.strictLimitsClosureStep_strictLimitsClosureIter_eq_self, enumOrd_isNormal_iff_isClosed, isNormal_veblenWith', Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, Profinite.NobelingProof.CC_comp_zero, Profinite.NobelingProof.CC_exact, Cardinal.isNormal_beth, isNormal_add_right, Profinite.NobelingProof.injective_ฯs, Profinite.NobelingProof.coe_ฯs', Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, Cardinal.isNormal_preBeth, Cardinal.isNormal_ord, Profinite.NobelingProof.Products.eval_ฯs_image, IsNormal.trans, isNormal_iff_strictMono_and_continuous, isNormal_omega, Profinite.NobelingProof.succ_mono
|
instOrderBot ๐ | CompOp | 2 mathmath: bot_eq_zero, boundedLimitRec_zero
|
instSuccAddOrder ๐ | CompOp | โ |
instSuccOrder ๐ | CompOp | 109 mathmath: succ_nmul, lt_omega0_opow_succ, boundedLimitRec_succ, Acc.rank_eq, pred_succ, add_succ, sup_eq_lsub_iff_succ, Cardinal.aleph_succ, iSup_typein_succ, succ_one, bsup_id_succ, sup_succ_le_lsub, PSet.le_succ_rank_sUnion, div_le, cof_eq_one_iff_is_succ, lt_mul_succ_div, nfp_mul_opow_omega0_add, one_add_ofNat, deriv_succ, succ_zero, bsup_succ_eq_blsub, lsub_const, nmul_succ, pred_le_iff_le_succ, Cardinal.beth_succ, PSet.rank_insert, lift_succ, iSup_eq_lsub_or_succ_iSup_eq_lsub, sup_succ_eq_lsub, succ_log_def, ZFSet.rank_powerset, derivFamily_succ, isNormal_iff_lt_succ_and_bsup_eq, lt_opow_succ_log_self, bsup_eq_blsub_iff_succ, zero_or_succ_or_isSuccLimit, cof_succ, Cardinal.isRegular_aleph_succ, le_enum_succ, mul_succ, limitRecOn_succ, epsilon_succ_eq_nfp, lt_div, isNormal_iff_lt_succ_and_blsub_eq, CategoryTheory.ObjectProperty.isoClosure_strictLimitsClosureIter_eq_limitsClosure, isInitial_succ, natCast_succ, bsup_eq_blsub_or_succ_bsup_eq_blsub, one_nadd, mul_eq_opow_log_succ, opow_mul_add_lt_opow_succ, Cardinal.preAleph_succ, enum_succ_eq_top, IsNormal.eq_iff_zero_and_succ, PSet.rank_powerset, Cardinal.preBeth_succ, IsWellFounded.rank_eq, log_eq_iff, bsup_succ_of_mono, ZFSet.rank_range, enumOrd_succ_le, ZFSet.rank_insert, card_succ, PSet.rank_singleton, bsup_succ_le_blsub, succ_iSup_eq_lsub_iff, lt_pred_iff_succ_lt, ONote.fundamentalSequenceProp_inl_some, sup_eq_lsub, blsub_succ_of_mono, veblenWith_succ, ZFSet.mem_vonNeumann_succ, IsFundamentalSequence.succ, nadd_succ, CategoryTheory.ObjectProperty.strictLimitsClosureStep_strictLimitsClosureIter_eq_self, lsub_le_succ_iSup, bsup_eq_blsub, add_mul_succ, blsub_const, bsup_not_succ_of_ne_bsup, blsub_one, succ_pos, ONote.repr_opow_auxโ, succ_pred_eq_iff_not_isSuccPrelimit, sup_eq_lsub_or_sup_succ_eq_lsub, veblen_succ, opow_succ, add_one_eq_succ, ZFSet.rank_pair, opow_mul_add_lt_opow_mul_succ, toZFSet_succ, opow_lt_opow_left_of_succ, iSup_eq_lsub, iSup_eq_lsub_iff, ZFSet.rank_singleton, self_le_succ_pred, blsub_le_bsup_succ, lsub_unique, lsub_le_sup_succ, ZFSet.vonNeumann_succ, succ_iSup_le_lsub_iff, succ_nadd, nadd_one, ZFSet.le_succ_rank_sUnion, PSet.rank_pair, gamma_succ_eq_nfp, sup_typein_succ, Cardinal.isRegular_preAleph_succ, succ_lt_iSup_of_ne_iSup
|
instSuccOrderToType ๐ | CompOp | 19 mathmath: CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, CategoryTheory.OrthogonalReflection.iteration_map_succ, CategoryTheory.SmallObject.ฮนFunctorObj_eq, CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, CategoryTheory.SmallObject.ฯFunctorObj_eq, CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument', CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ฮนIteration_app_right, CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropฮนIteration_F, CategoryTheory.SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument', CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit, CategoryTheory.SmallObject.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ฮนObj, CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, CategoryTheory.SmallObject.preservesColimit, CategoryTheory.SmallObject.iterationFunctorObjObjRightIso_ฮนIteration_app_right_assoc
|
isEquivalent ๐ | CompOp | 1 mathmath: relIso_enum
|
liftInitialSeg ๐ | CompOp | 1 mathmath: liftInitialSeg_coe
|
liftOnWellOrder ๐ | CompOp | 1 mathmath: liftOnWellOrder_type
|
liftPrincipalSeg ๐ | CompOp | 3 mathmath: liftPrincipalSeg_top', liftPrincipalSeg_coe, liftPrincipalSeg_top
|
omega0 ๐ | CompOp | 106 mathmath: Cardinal.preBeth_omega, lt_omega0_opow_succ, iSup_pow_natCast, invVeblenโ_eq_iff, ONote.nf_repr_split', omega0_lt_omega_one, le_invVeblenโ_iff, deriv_add_eq_mul_omega0_add, omega0_lt_preOmega_iff, omega_zero, Cardinal.ord_aleph0, isSuccLimit_omega0, epsilon_eq_deriv, card_omega0, range_omega, principal_mul_omega0, principal_opow_omega0, invVeblenโ_le_iff, card_omega0_opow, natCast_mul_omega0, iSup_pow, ONote.split_dvd, omega0_pos, eq_zero_or_opow_omega0_le_of_mul_eq_right, SetTheory.PGame.short_birthday, one_add_omega0, iSup_add_nat, Cardinal.preAleph_omega0, mem_range_omega_iff, veblen_opow_eq_opow_iff, eq_nat_or_omega0_le, iSup_mul_nat, lt_epsilon_zero, iterate_omega0_opow_lt_epsilon0, ONote.repr_scale, omega0_le, iSup_add_natCast, veblen_zero, isInitial_omega0, mul_eq_right_iff_opow_omega0_dvd, ONote.omega0_le_oadd, Cardinal.omega0_le_ord, principal_add_iff_zero_or_omega0_opow, epsilon_succ_eq_nfp, Cardinal.ord_lt_omega0, iSup_mul_natCast, omega0_lt_omega1, card_opow_omega0, aleph0_le_card, isInitial_succ, mem_range_veblen_iff_le_invVeblenโ, add_eq_right_iff_mul_omega0_le, omega0_le_omega, ONote.split_add_lt, natCast_opow_omega0, Cardinal.aleph0_le_preAleph, veblen_invVeblenโ_invVeblenโ, lt_omega0_opow, omega0_lt_epsilon, epsilon0_eq_nfp, epsilon_zero_eq_nfp, veblen_mem_range_opow, omega0_le_preOmega_iff, omega0_lt_gamma, deriv_mul_eq_opow_omega0_mul, opow_lt_veblen_opow_iff, principal_add_omega0, natCast_mod_omega0, mul_le_right_iff_opow_omega0_dvd, IsNormal.apply_omega0, type_nat_lt, principal_mul_omega0_opow_opow, omega0_opow_mul_nat_lt, nat_lt_omega0, invVeblenโ_lt_iff, Cardinal.beth_eq_preBeth, lift_omega0, Cardinal.omega0_lt_ord, Cardinal.aleph_eq_preAleph, invVeblenโ_lt, lt_omega0, lt_invVeblenโ_iff, veblen_eq_opow_iff, principal_add_omega0_opow, nfp_mul_one, veblen_zero_apply, card_lt_aleph0, omega0_le_of_isSuccLimit, nfp_add_zero, preOmega_omega0, ONote.scale_opowAux, iSup_natCast, add_le_right_iff_mul_omega0_le, iterate_omega0_opow_lt_epsilon_zero, Cardinal.ord_le_omega0, apply_omega0_of_isNormal, Cardinal.ord_eq_omega0, cof_omega0, natCast_add_omega0, one_lt_omega0, isSuccLimit_iff_omega0_dvd, ONote.NFBelow.repr_lt, principal_mul_iff_le_two_or_omega0_opow_opow, lt_epsilon0, omega0_opow_epsilon, omega_eq_preOmega
|
one ๐ | CompOp | 115 mathmath: SetTheory.PGame.default_nim_one_rightMoves_eq, opow_one, lift_one, Iio_one_default_eq, one_nmul, omega0_lt_omega_one, nadd_one_nmul, toNatOrdinal_eq_one, succ_one, Cardinal.lift_eq_aleph_one, SetTheory.PGame.birthday_one, card_one, Nimber.succ_def, one_toPGame_leftMoves_default_eq, toGame_one, nmul_add_one, one_add_ofNat, log_one_left, SetTheory.PGame.nim_one_equiv, div_self, Cardinal.aleph_one_le_continuum, NatOrdinal.succ_def, nmul_nadd_one, succ_zero, SetTheory.PGame.toRightMovesNim_one_symm, Cardinal.preBeth_one, zero_opow', one_add_omega0, instZeroLEOneClass, lt_one_iff_zero, SetTheory.Game.birthday_one, one_add_of_omega0_le, opow_one_add, Cardinal.aleph1_le_lift, card_le_one, toPGame_one, OrdinalApprox.gfpApprox_add_one, SetTheory.PGame.birthday_star, cardinalInterFilter_aleph_one_iff, isInitial_one, Cardinal.ord_eq_one, mod_one, Cardinal.beth_one, toNatOrdinal_one, bsup_one, SetTheory.PGame.nim_one_moveLeft, one_lt_card, SetTheory.PGame.default_nim_one_leftMoves_eq, one_opow, Cardinal.aleph1_lt_lift, type_eq_one_iff_unique, one_toPGame_moveLeft, Cardinal.lift_eq_aleph1, zero_opow_le, OrdinalApprox.lfpApprox_add_one, one_add_natCast, toNimber_one, omega0_lt_omega1, Nimber.toOrdinal_eq_one, one_nadd, Nimber.toOrdinal_one, Cardinal.aleph_one_le_lift, principal_one_iff, Cardinal.lift_le_aleph1, CNF.coeff_one_left, Cardinal.ord_one, type_pUnit, principal_add_one, CNF.one_left, card_eq_one, Cardinal.aleph0_lt_aleph_one, opow_zero, nmul_one, Cardinal.isRegular_aleph_one, IsFundamentalSequence.succ, Cardinal.lift_le_aleph_one, one_le_iff_ne_zero, type_unit, SetTheory.Game.birthday_star, one_lt_of_isSuccLimit, type_eq_one_of_unique, Cardinal.aleph1_eq_lift, NatOrdinal.toOrdinal_one, MeasurableSpace.generateMeasurableRec_omega_one, blsub_one, SetTheory.PGame.nim_one_moveRight, typein_one_toType, toNimber_eq_one, to_leftMoves_one_toPGame_symm, CountableInterFilter.toCardinalInterFilter, Cardinal.aleph_one_eq_lift, Cardinal.countable_iff_lt_aleph_one, nfp_mul_one, add_one_eq_succ, MeasurableSpace.generateMeasurableRec_omega1, one_CNF, Cardinal.lift_lt_aleph1, Cardinal.aleph_one_lt_lift, le_one_iff, invVeblenโ_epsilon, NatOrdinal.toOrdinal_eq_one, principal_mul_one, one_lt_omega0, one_le_card, nadd_one, Cardinal.succ_aleph0, add_one_nmul, div_one, Cardinal.lift_lt_aleph_one, ONote.nfBelow_ofNat, instNeZeroOne, SetTheory.PGame.toLeftMovesNim_one_symm, one_toType_eq, MeasurableSpace.generateMeasurable_eq_rec, log_one_right
|
partialOrder ๐ | CompOp | 687 mathmath: Cardinal.lt_ord_succ_card, isSuccLimit_lift, PSet.rank_le_iff, succ_nmul, Cardinal.aleph_le_beth, veblenWith_le_veblenWith_iff_right, lt_omega0_opow_succ, toNimber_eq_zero, isNormal_iff_strictMono_limit, Cardinal.mk_iUnion_Ordinal_le_of_le, principal_add_omega, SetTheory.PGame.default_nim_one_rightMoves_eq, Acc.rank_eq, toPGame_lf_iff, sup_eq_lsub_iff_lt_sup, ZFSet.IsOrdinal.rank_le_iff_subset, SetTheory.Game.birthday_add_le, ZFSet.subset_vonNeumann, lift_type_lt, sInf_compl_lt_lift_ord_succ, typein_le_typein, pred_succ, mem_range_typein_iff, IsAcc.isSuccLimit, gamma_le_gamma, add_succ, Cardinal.isStrongLimit_preBeth, card_le_ofNat, Iio_one_default_eq, lsub_pos, nmul_le_iffโ, sup_eq_lsub_iff_succ, Cardinal.aleph_succ, isInitialIso_apply, not_bddAbove_fp_family, blsub_congr, Cardinal.aleph_pos, liftInitialSeg_coe, iSup_typein_succ, existsAddOfLE, mul_le_nmul, blsub_le_iff, Cardinal.isSuccLimit_ord, omega_lt_omega, omega0_lt_omega_one, le_invVeblenโ_iff, toNatOrdinal_eq_one, type_lt_iff, IsNormal.apply_le_nfp, succ_one, sub_eq_zero_iff_le, Cardinal.ord.orderEmbedding_coe, omega0_lt_preOmega_iff, mulRightMono, instAddRightMono, Profinite.NobelingProof.coe_ฯs, lift_lt, SetTheory.Game.birthday_sub_le, ZFSet.lt_rank_iff, apply_le_nfp, mod_le, Cardinal.lift_eq_aleph_one, SetTheory.PGame.grundyValue_eq_iff_equiv_nim, not_lt_zero, card_le_aleph, isAcc_iff, omega_zero, toNimber_symm_eq, bsup_id_succ, liftPrincipalSeg_top', sup_succ_le_lsub, iSup_le_lsub, card_iSup_Iio_le_sum_card, isOpen_singleton_iff, NatOrdinal.toOrdinal_min, enum_symm_apply_coe, toGame_lt_iff, IsNormal.lt_iff, SetTheory.PGame.grundyValue_nim_add_nim, Nimber.succ_def, deriv_strictMono, enum_zero_le, PSet.le_succ_rank_sUnion, lt_mul_div_add, omega_le_omega, IsNormal.nfp_le_apply, enum_lt_enum, isSuccLimit_omega0, isInitialIso_symm_apply_coe, isInitial_preOmega, add_log_le_log_mul, Cardinal.isNormal_preAleph, Cardinal.bddAbove_ord_image_iff, SetTheory.PGame.birthday_moveLeft_lt, epsilon_zero_lt_gamma, div_le, one_toPGame_leftMoves_default_eq, toGame_one, Cardinal.preAleph_nat, PSet.rank_mono, toNimber_min, Mathlib.Meta.NormNum.isNat_ordinalLT_true, le_add_left, pred_le_self, cof_eq_one_iff_is_succ, ZFSet.vonNeumann_subset_vonNeumann_iff, div_lt, range_omega, not_bddAbove_isInitial, lt_mul_succ_div, div_opow_log_pos, one_add_ofNat, nadd_le_nadd_iff_right, isOpen_iff, Nimber.toOrdinal_max, le_iff_derivFamily, Cardinal.preAleph_le_aleph, CNF.sorted, type_le_iff, opow_mul_add_pos, log_le_self, coe_toZFSet, typein_top, Nimber.toOrdinal_min, invVeblenโ_le_iff, enum_le_enum', apply_lt_nfpFamily_iff, deriv_succ, bfamilyOfFamily'_typein, invVeblenโ_le, Cardinal.aleph_one_le_continuum, WellFoundedGT.rank_strictAnti, NatOrdinal.succ_def, veblenWith_right_strictMono, nadd_le_nadd_iff_left, succ_zero, card_le_preAleph, Cardinal.aleph_mul_aleph0, SetTheory.PGame.toRightMovesNim_one_symm, Profinite.NobelingProof.GoodProducts.smaller_factorization, lt_nfpFamily_iff, omega0_pos, not_bddAbove_principal, eq_zero_or_opow_omega0_le_of_mul_eq_right, Cardinal.card_le_iff, SetTheory.PGame.short_birthday, liftPrincipalSeg_coe, NatOrdinal.bot_eq_zero, Besicovitch.TauPackage.monotone_iUnionUpTo, bsup_succ_eq_blsub, opow_log_le_self, Cardinal.aleph_add_aleph, le_nadd_self, instZeroLEOneClass, lsub_const, lt_one_iff_zero, nmul_succ, toNatOrdinal_min, isSuccLimit_add_iff, Cardinal.preAleph_omega0, lt_gamma0, foldr_le_nfpFamily, bot_eq_zero, PSet.rank_lt_of_mem, pred_le_iff_le_succ, Cardinal.beth_succ, mem_range_omega_iff, nat_le_card, mem_toZFSet_iff, SetTheory.PGame.lt_birthday_iff, ZFSet.rank_mono, Acc.rank_lt_of_rel, Cardinal.lt_omega_iff_card_lt, ONote.lt_def, veblen_zero_lt_veblen_zero, Cardinal.le_preAleph_ord, Cardinal.aleph1_le_lift, typein_lt_type, apply_lt_nfp, PSet.rank_insert, toZFSet_strictMono, card_le_one, lt_sub, lift_succ, veblen_of_ne_zero, iSup_eq_lsub_or_succ_iSup_eq_lsub, sup_succ_eq_lsub, type_le_iff', Cardinal.le_aleph_ord, ONote.NFBelow.lt, IsInitial.card_lt_card, NatOrdinal.toOrdinal_max, typein_lt_typein, eq_nat_or_omega0_le, iterate_veblen_lt_gamma0, cardinalInterFilter_aleph_one_iff, nat_lt_card, IsWellFounded.rank_lt_of_rel, ZFSet.rank_powerset, lt_nmul_iffโ, lt_epsilon_zero, le_zero, iterate_omega0_opow_lt_epsilon0, lt_nmul_iff, instPosMulStrictMono, derivFamily_succ, le_self_nadd, IsNormal.id_le, isNormal_iff_lt_succ_and_bsup_eq, Cardinal.aleph_le_aleph, IsNormal.le_apply, lt_add_iff, SetTheory.Game.birthday_ordinalToGame, Profinite.NobelingProof.contained_eq_proj, SetTheory.Game.le_birthday, iterate_le_nfp, IsWellFounded.rank_eq_typein, PSet.rank_sUnion_le, isSuccPrelimit_zero, CNF_sorted, IsNormal.apply_lt_nfp, le_nfp, omega0_le, bsup_eq_blsub_iff_succ, SetTheory.PGame.moveRight_nim, toNatOrdinal_one, sup_le_lsub, bsup_one, Cardinal.beth_le_beth, IsNormal.le_iff, mod_lt, PrincipalSeg.ordinal_type_lt, not_bddAbove_fp, card_iSup_Iio_le_card_mul_iSup, zero_or_succ_or_isSuccLimit, nfp_le_iff, Cardinal.ord_aleph, small_Iic, Nimber.add_nat, nfp_le_apply, wellFoundedLT, veblenWith_lt_veblenWith_iff, card_lt_nat, ZFSet.mem_vonNeumann', derivFamily_strictMono, blsub_le_of_brange_subset, ZFSet.vonNeumann_mem_vonNeumann_iff, one_lt_card, lt_blsub_iff, Cardinal.ord_le, isNormal_preOmega, preOmega_ofNat, SetTheory.PGame.default_nim_one_leftMoves_eq, preOmega_le_omega, cof_succ, ZFSet.vonNeumann_strictMono, type_subrel, Cardinal.isRegular_aleph_succ, Cardinal.ord_le_ord, Cardinal.beth_mono, gamma_pos, lt_lift_iff, OrdinalApprox.lfpApprox_monotone, principal_mul_omega, Cardinal.aleph1_lt_lift, le_enum_succ, OrdinalApprox.gfpApprox_antitone, mem_toPSet_iff, Cardinal.isNormal_aleph, mul_succ, cmp_veblen, ONote.omega0_le_oadd, Cardinal.omega0_le_ord, enum_typein, instAddLeftReflectLT, limitRecOn_succ, sub_le, instAddLeftStrictMono, Cardinal.card_typein_lt, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, Cardinal.card_typein_toType_lt, blsub_type, Cardinal.lift_eq_aleph1, zero_opow_le, instOrderTopology, bddAbove_range, NatOrdinal.toOrdinal_natCast, SetTheory.PGame.equiv_nim_grundyValue, Mathlib.Meta.NormNum.isNat_ordinalLT_false, epsilon_succ_eq_nfp, Cardinal.preBeth_lt_preBeth, lt_div, ONote.le_def, veblenWith_lt_veblenWith_iff_right, Cardinal.ord_lt_omega0, not_principal_iff, IsNormal.monotone, Cardinal.aleph_max, toNimber_one, Cardinal.ord_preAleph, omega0_lt_omega1, bfamilyOfFamily_typein, pred_lt_iff_not_isSuccPrelimit, mk_toPGame, isNormal_iff_lt_succ_and_blsub_eq, Cardinal.isStrongLimit_beth, preOmega_zero, aleph0_le_card, isInitial_succ, natCast_succ, coe_preOmega, veblen_zero_le_veblen_zero, Cardinal.preAleph_max, typein_injective, ord_cof_le, Cardinal.preBeth_le_preBeth, toZFSetIso_apply, Nimber.toOrdinal_eq_one, bsup_le_of_brange_subset, nadd_le_iff, mem_range_veblen_iff_le_invVeblenโ, add_eq_right_iff_mul_omega0_le, omega0_le_omega, mem_closure_tfae, bsup_eq_blsub_or_succ_bsup_eq_blsub, ONote.split_add_lt, not_isSuccLimit_zero, toGame_zero, isSuccLimit_iff, veblen_eq_veblen_iff, add_le_nadd, pred_eq_iff_isSuccPrelimit, mod_opow_log_lt_self, mk_Iio_ordinal, bddAbove_of_small, Profinite.NobelingProof.ฯs_apply_apply, card_le_nat, typein_apply, lsub_le_of_range_subset, one_nadd, ToType.mk_symm_apply_coe, Cardinal.range_aleph, bddAbove_iff_small, Cardinal.aleph0_le_preAleph, Cardinal.preAleph_succ, strictMono_gamma, enum_succ_eq_top, Nimber.toOrdinal_one, iterate_veblen_lt_gamma_zero, typein_surjOn, lt_omega0_opow, Cardinal.aleph_one_le_lift, IsNormal.eq_iff_zero_and_succ, OrdinalApprox.exists_gfpApprox_eq_gfpApprox, PSet.rank_powerset, isInitial_omega, epsilon0_lt_gamma, omega0_lt_epsilon, Cardinal.preBeth_succ, Mathlib.Meta.NormNum.isNat_ordinalLE_true, IsWellFounded.rank_eq, Cardinal.not_injective_limitation_set, veblen_le_veblen_iff, bsup_congr, eq_zero_or_pos, small_Icc, veblen_le_veblen_iff_right, ofNat_lt_card, Cardinal.lift_le_aleph1, Cardinal.gc_ord_card, ZFSet.rank_range, toGame_nmul, bsup_eq_blsub_iff_lt_bsup, le_preOmega_self, isSuccPrelimit_lift, WellFoundedLT.rank_strictMono, ZFSet.rank_insert, toGame_lf_iff, enum_le_enum, Cardinal.preAleph_zero, lsub_le_iff, lt_wf, card_succ, sub_le_self, aleph0_le_cof, le_iSup, card_omega, Profinite.NobelingProof.isClosed_proj, card_typein, lift_typein_top, Cardinal.IsRegular.ord_pos, typein_ordinal, apply_le_nfpFamily, Cardinal.lift_aleph, toNatOrdinal_zero, div_pos, PSet.rank_singleton, exists_lt_add_of_not_principal_add, ofNat_le_card, NatOrdinal.toOrdinal_eq_zero, omega0_le_preOmega_iff, IsFundamentalSequence.ord_cof, invVeblenโ_le, mulLeftMono, instNoMaxOrder, bsup_succ_le_blsub, lift_preOmega, succ_iSup_eq_lsub_iff, omega0_lt_gamma, Cardinal.aleph0_le_aleph, zero_lt_card, lift_type_le, IsInitial.card_le_card, Cardinal.preAleph_le_preAleph, small_Ioc, omega_strictMono, toPGame_lt_iff, lt_pred_iff_succ_lt, ONote.fundamentalSequenceProp_inl_some, sup_eq_lsub, veblenWith_le_veblenWith_iff, iSup_eq_lsub_iff_lt_iSup, cmp_veblenWith, lsub_typein, ONote.NF.of_dvd_omega0_opow, lt_gamma_zero, Cardinal.aleph0_lt_aleph_one, IsNormal.strictMono, lt_bsup_of_ne_bsup, RelEmbedding.ordinal_type_le, opow_lt_veblen_opow_iff, toNatOrdinal_eq_zero, SetTheory.Game.small_setOf_birthday_lt, bsup_le_iff, veblenWith_succ, lt_veblen_iff_invVeblenโ_le, SetTheory.PGame.toLeftMovesNim_symm_lt, toGame_inj, Cardinal.preAleph_lt_preAleph, univ_id, gamma_lt_gamma, lt_iSup_iff, Cardinal.aleph_mul_aleph, CNF.lt_snd, Cardinal.beth_strictMono, SetTheory.Game.neg_birthday_le, Cardinal.isRegular_aleph_one, ZFSet.mem_vonNeumann_succ, instAddLeftReflectLE, ZFSet.rank_le_iff, le_lift_iff, iSup_Iio_eq_bsup, IsFundamentalSequence.succ, Profinite.NobelingProof.contained_proj, Cardinal.lift_le_aleph_one, SetTheory.PGame.moveLeft_toLeftMovesNim, nfpFamily_le_iff, MeasurableSpace.generateMeasurableRec_mono, ONote.repr_le_repr, one_le_iff_ne_zero, nadd_succ, veblen_lt_veblen_iff, instIsEmptyIioZero, lt_nfp_iff, ONote.fundamentalSequenceProp_inr, invVeblenโ_lt_iff, ONote.repr_lt_repr, toPGame_moveLeft, preOmega_strictMono, SetTheory.PGame.birthday_moveRight_lt, ZFSet.mem_vonNeumann, principal_opow_omega, PSet.lt_rank_iff, card_preOmega, lsub_le_succ_iSup, typein_lt_self, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, lt_veblen, toZFSet_subset_toZFSet_iff, nat_lt_omega0, invVeblenโ_lt_iff, toNatOrdinal_natCast, NatOrdinal.toOrdinal_symm_eq, Cardinal.aleph1_eq_lift, ZFSet.rank_sUnion_le, NatOrdinal.toOrdinal_one, lt_lsub, toNimber_zero, bsup_eq_blsub, NatOrdinal.toOrdinal_toNatOrdinal, sInf_compl_lt_ord_succ, Cardinal.ord_strictMono, add_mul_succ, Cardinal.preAleph_le_preBeth, MeasurableSpace.generateMeasurableRec_omega_one, Cardinal.ord_lt_ord, blsub_const, ZFSet.rank_lt_of_mem, small_Ioo, Cardinal.preAleph_pos, Cardinal.beth_lt_beth, ToType.mk_apply, blsub_one, small_Iio, toPGame_moveLeft_hEq, Cardinal.omega0_lt_ord, typein_one_toType, succ_pos, toNimber_toOrdinal, toNimber_max, canonicallyOrderedAdd, bsup_le_blsub, toZFSet_monotone, mem_range_preOmega_iff, omega_max, CNF.fst_le_log, toNimber_eq_one, Profinite.NobelingProof.Products.prop_of_isGood_of_contained, Cardinal.aleph_eq_preAleph, omega_pos, invVeblenโ_lt, to_leftMoves_one_toPGame_symm, lt_omega0, le_add_right, nadd_lt_nadd_iff_right, lt_invVeblenโ_iff, add_le_iff, Cardinal.preBeth_strictMono, veblen_right_strictMono, typein_le_typein', succ_pred_eq_iff_not_isSuccPrelimit, toGame_injective, CountableInterFilter.toCardinalInterFilter, Cardinal.aleph_one_eq_lift, enum_inj, sup_eq_lsub_or_sup_succ_eq_lsub, Nimber.toOrdinal_symm_eq, Profinite.NobelingProof.injective_ฯs, Cardinal.aleph_toENat, Cardinal.preBeth_mono, Cardinal.countable_iff_lt_aleph_one, SetTheory.Game.birthday_quot_le_pGameBirthday, veblen_succ, instAddLeftMono, opow_succ, add_one_eq_succ, card_lt_aleph0, nfpFamily_le_apply, IsAcc.pos, IsNormal.le_iff_deriv, Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, ZFSet.rank_pair, add_le_add_iff_right, SetTheory.PGame.nim_grundyValue, MeasurableSpace.generateMeasurableRec_omega1, ZFSet.IsOrdinal.rank_lt_iff_mem, toZFSet_succ, preOmega_le_preOmega, veblenWith_eq_veblenWith_iff, epsilon_pos, CNF_fst_le_log, lift_omega, preOmega_omega0, card_lt_ofNat, iSup_le_iff, Cardinal.aleph0_mul_aleph, preOmega_lt_preOmega, left_le_veblen, Cardinal.lift_lt_aleph1, Cardinal.ord_card_le, iSup_eq_lsub, not_bddAbove_compl_of_small, Cardinal.mk_biUnion_le_of_le, veblen_lt_veblen_iff_right, nmul_le_iff, lt_bsup, iSup_eq_lsub_iff, toPGame_le_iff, Nimber.toOrdinal_zero, NatOrdinal.toOrdinal_zero, ZFSet.rank_singleton, add_le_right_iff_mul_omega0_le, iterate_omega0_opow_lt_epsilon_zero, Cardinal.isSuccLimit_omega, Mathlib.Meta.NormNum.isNat_ordinalLE_false, Cardinal.ord_le_omega0, self_le_succ_pred, Cardinal.aleph_one_lt_lift, typein_inj, veblenWith_of_ne_zero, SetTheory.PGame.moveRight_nim_heq, sub_ne_zero_iff_lt, Nimber.toOrdinal_toNimber, le_one_iff, natCast_lt_epsilon, InitialSeg.ordinal_type_le, instAddRightReflectLT, Cardinal.mk_iUnion_Ordinal_lift_le_of_le, lt_veblen_invVeblenโ, toNatOrdinal_toOrdinal, SetTheory.PGame.moveLeft_nim_heq, preOmega_natCast, blsub_le_bsup_succ, Cardinal.preBeth_pos, IsNormal.le_iff_eq, toLeftMovesToPGame_symm_lt, toZFSetIso_symm_apply, Cardinal.ord_le_type, isSuccLimit_of_mem_frontier, lsub_unique, NatOrdinal.toOrdinal_eq_one, SetTheory.PGame.moveLeft_nim, lt_nadd_iff, Cardinal.mem_range_aleph_iff, lsub_le_sup_succ, Cardinal.ord_mono, Cardinal.aleph_lt_aleph, CNF_lt_snd, Cardinal.mk_biUnion_le_of_le_lift, ZFSet.vonNeumann_succ, nmul_eq_mul, succ_iSup_le_lsub_iff, toZFSet_mem_toZFSet_iff, le_div, small_Ico, IsInitial.mem_range_preOmega, Cardinal.lt_ord, nhds_eq_pure, succ_nadd, Cardinal.aleph_toNat, range_preOmega, one_lt_omega0, preOmega_max, one_le_card, nadd_one, SetTheory.PGame.nim_add_nim_equiv, veblen_zero_strictMono, le_add_sub, toGame_nadd, SetTheory.PGame.moveRight_toRightMovesNim, right_le_veblen, Cardinal.succ_aleph0, toNatOrdinal_max, ZFSet.le_succ_rank_sUnion, Nimber.toOrdinal_eq_zero, le_iff_deriv, natCast_lt_gamma, toGame_natCast, toPGameEmbedding_apply, PSet.rank_pair, le_omega_self, Cardinal.aleph_zero, lift_le, isNormal_iff_strictMono_and_continuous, isSuccLimit_iff_omega0_dvd, gamma_succ_eq_nfp, lt_lsub_iff, veblenWith_left_monotone, SetTheory.PGame.toRightMovesNim_symm_lt, ONote.NFBelow.repr_lt, le_of_dvd, le_nfpFamily, principal_mul_iff_le_two_or_omega0_opow_opow, lt_epsilon0, toGame_le_iff, veblen_pos, Cardinal.lift_preAleph, omega_eq_preOmega, Cardinal.lift_lt_aleph_one, toNatOrdinal_symm_eq, monotone_gamma, mul_div_le, top_typein, SetTheory.PGame.toLeftMovesNim_one_symm, sup_typein_succ, liftPrincipalSeg_top, enum_type, nadd_lt_nadd_iff_left, right_le_veblenWith, nadd_eq_add, one_toType_eq, isNormal_omega, MeasurableSpace.generateMeasurable_eq_rec, toPGame_moveLeft', Profinite.NobelingProof.succ_mono, apply_lt_veblenWith_apply_iff, veblen_left_monotone
|
principalSegToType ๐ | CompOp | โ |
termTypeLT_ ๐ | CompOp | โ |
termฯ ๐ | CompOp | โ |
toType ๐ | CompOp | โ |
toTypeOrderBot ๐ | CompOp | โ |
type ๐ | CompOp | 76 mathmath: type_eq, lift_type_lt, mem_range_typein_iff, type_uLift, liftOnWellOrder_type, type_lt_iff, liftPrincipalSeg_top', enum_symm_apply_coe, blsub_eq_blsub, enum_zero_le, enum_lt_enum, cof_type, type_le_iff, typein_top, brange_bfamilyOfFamily', enum_le_enum', lift_type_eq, type_eq_zero_of_empty, typein_lt_type, type_le_iff', RelIso.ordinal_lift_type_eq, PrincipalSeg.ordinal_type_lt, Cardinal.ord_eq_Inf, type_subrel, le_enum_succ, type_eq_one_iff_unique, enum_typein, blsub_type, type_pEmpty, bsup_eq_sup, type_prod_lex, Cardinal.type_cardinal, type_fintype, enum_succ_eq_top, typein_surjOn, cof_type_le, enum_le_enum, ord_cof_eq, lift_typein_top, brange_bfamilyOfFamily, type_lift_preimage, type_pUnit, card_type, lift_type_le, RelEmbedding.ordinal_type_le, enum_zero_eq_bot, univ_id, bsup'_eq_iSup, type_empty, type_nat_lt, type_unit, bsup_eq_iSup, RelIso.ordinal_type_eq, type_eq_one_of_unique, type_sum_lex, bsup_eq_sup', Cardinal.ord_eq, ToType.mk_apply, cof_type_lt, cof_eq, blsub_eq_lsub, enum_inj, blsub_eq_lsub', bsup_eq_bsup, type_eq_zero_iff_isEmpty, InitialSeg.ordinal_type_le, enum_zero_le', Cardinal.ord_le_type, familyOfBFamily_enum, type_toType, le_cof_type, type_fin, top_typein, enum_type, one_toType_eq, type_preimage
|
typein ๐ | CompOp | 33 mathmath: typein_le_typein, mem_range_typein_iff, iSup_typein_succ, enum_symm_apply_coe, typein_top, bfamilyOfFamily'_typein, typein_lt_type, typein_lt_typein, IsWellFounded.rank_eq_typein, type_subrel, enum_typein, Cardinal.card_typein_lt, Cardinal.card_typein_toType_lt, blsub_type, bfamilyOfFamily_typein, typein_enum, typein_surj, typein_injective, typein_apply, ToType.mk_symm_apply_coe, typein_surjOn, iSup_typein_limit, card_typein, lift_typein_top, typein_ordinal, lsub_typein, typein_lt_self, typein_one_toType, sup_typein_limit, typein_le_typein', typein_inj, top_typein, sup_typein_succ
|
uniqueIioOne ๐ | CompOp | 1 mathmath: Iio_one_default_eq
|
uniqueToTypeOne ๐ | CompOp | โ |
univ ๐ | CompOp | 8 mathmath: Cardinal.ord_univ, cof_univ, Cardinal.type_cardinal, univ_id, univ_umax, card_univ, lift_univ, liftPrincipalSeg_top
|
wellFoundedRelation ๐ | CompOp | โ |
zero ๐ | CompOp | 208 mathmath: toNimber_eq_zero, SetTheory.PGame.default_nim_one_rightMoves_eq, zero_nadd, sub_zero, max_zero_left, Iio_one_default_eq, lsub_pos, Cardinal.preBeth_eq_zero, ONote.NFBelow_zero, noZeroDivisors, cof_zero, log_of_left_le_one, sub_eq_zero_iff_le, mod_self, CNF.coeff_zero_left, ZFSet.rank_empty, not_lt_zero, gamma_zero_eq_nfp, invVeblenโ_zero, omega_zero, CNF_foldr, enum_zero_le, card_zero, SetTheory.PGame.isEmpty_nim_zero_leftMoves, invVeblenโ_zero, epsilon_zero_lt_gamma, log_zero_right, one_toPGame_leftMoves_default_eq, log_zero_left, toPGame_zero, log_eq_zero, veblen_gamma_zero, div_opow_log_pos, CNF.zero_left, log_one_left, Cardinal.ord_eq_zero, limitRecOn_zero, opow_mul_add_pos, CNF.coeff_zero_apply, succ_zero, SetTheory.PGame.toRightMovesNim_one_symm, epsilon_zero_le_of_omega0_opow_le, zero_opow', omega0_pos, zero_sub, isEmpty_zero_toPGame_leftMoves, eq_zero_or_opow_omega0_le_of_mul_eq_right, CNF.coeff_of_not_mem_CNF, instZeroLEOneClass, lt_one_iff_zero, isSuccLimit_add_iff, lt_gamma0, Profinite.NobelingProof.GoodProducts.P0, bot_eq_zero, type_eq_zero_of_empty, SetTheory.Game.birthday_zero, zero_CNF, CNF.of_lt, mul_mod, veblen_zero_lt_veblen_zero, CNFRec_zero, CNF.coeff_of_mem_CNF, enumOrd_zero, iterate_veblen_lt_gamma0, lt_epsilon_zero, boundedLimitRec_zero, le_zero, iterate_omega0_opow_lt_epsilon0, card_eq_zero, instPosMulStrictMono, mod_one, sub_self, invVeblenโ_of_lt_opow, isSuccPrelimit_zero, ONote.repr_zero, bsup_one, nfp_mul_zero, zero_or_succ_or_isSuccLimit, Cardinal.preBeth_zero, SetTheory.PGame.nim_one_moveLeft, bsup_zero, nfp_zero, Cardinal.ord_zero, div_eq_zero_of_lt, Cardinal.beth_zero, SetTheory.PGame.default_nim_one_leftMoves_eq, SetTheory.Game.birthday_eq_zero, invVeblenโ_gamma, veblen_zero, gamma_pos, add_eq_zero_iff, one_toPGame_moveLeft, SetTheory.PGame.birthday_zero, dvd_iff_mod_eq_zero, principal_add_iff_zero_or_omega0_opow, zero_opow_le, type_pEmpty, max_eq_zero, nmul_zero, CNF.of_le_one, ZFSet.vonNeumann_zero, preOmega_zero, PSet.rank_empty, veblen_zero_le_veblen_zero, isNormal_veblen_zero, CNF.rec_zero, mem_closure_tfae, isInitial_zero, not_isSuccLimit_zero, toGame_zero, deriv_zero, pred_zero, SetTheory.PGame.nim_zero_equiv, iterate_veblen_lt_gamma_zero, zero_nmul, IsNormal.eq_iff_zero_and_succ, epsilon0_lt_gamma, SetTheory.PGame.birthday_eq_zero, principal_one_iff, eq_zero_or_pos, zero_div, CNF.foldr, lift_zero, CNF.coeff_one_left, Cardinal.preAleph_zero, iSup_eq_zero_iff, Cardinal.IsRegular.ord_pos, epsilon0_eq_nfp, epsilon_zero_eq_nfp, toNatOrdinal_zero, div_pos, CNF.coeff_zero_right, NatOrdinal.toOrdinal_eq_zero, deriv_zero_left, mem_range_gamma, CNF.one_left, zero_lt_card, gamma0_eq_nfp, CNF_of_le_one, nfp_zero_left, lt_gamma_zero, opow_zero, mod_zero, toNatOrdinal_eq_zero, isEmpty_toType_zero, CNF.lt_snd, instIsEmptyIioZero, veblenWith_zero, type_empty, derivFamily_zero, epsilon0_le_of_omega0_opow_le, toNimber_zero, nadd_zero, Cardinal.preAleph_pos, blsub_one, SetTheory.PGame.nim_one_moveRight, typein_one_toType, CNF_of_lt, succ_pos, bsup_eq_zero_iff, omega_pos, to_leftMoves_one_toPGame_symm, toType_empty_iff_eq_zero, CNF.coeff_of_le_one, toZFSet_zero, mod_eq_zero_of_dvd, cof_eq_zero, veblen_zero_apply, deriv_zero_right, IsAcc.pos, blsub_eq_zero_iff, nfp_add_zero, epsilon_pos, one_CNF, log_pos, max_zero_right, blsub_zero, Nimber.toOrdinal_zero, NatOrdinal.toOrdinal_zero, lsub_empty, iterate_omega0_opow_lt_epsilon_zero, CNF_zero, type_eq_zero_iff_isEmpty, le_one_iff, lsub_eq_zero_iff, zero_opow, Cardinal.preBeth_pos, CNF_lt_snd, invVeblenโ_eq_iff, veblen_zero_inj, veblen_zero_strictMono, CNF.zero_right, IsFundamentalSequence.zero, Nimber.toOrdinal_eq_zero, Cardinal.aleph_zero, gamma_succ_eq_nfp, SetTheory.PGame.isEmpty_nim_zero_rightMoves, principal_zero, zero_mod, lt_epsilon0, veblen_pos, div_zero, instNeZeroOne, SetTheory.PGame.toLeftMovesNim_one_symm, sInf_empty, opow_eq_zero, one_toType_eq, log_one_right
|