| Name | Category | Theorems |
|---|
ToType 📖 | CompOp | 87 mathmath: iSup_eq_bsup, Field.Emb.Cardinal.equivLim_coherence, 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, nonempty_toType_iff, 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, Field.Emb.Cardinal.eq_bot_of_not_nonempty, cof_eq_cof_toType, CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc, comp_familyOfBFamily, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, ToType.mk_symm_apply_coe, Field.Emb.Cardinal.filtration_apply, enum_succ_eq_top, cof_toType, CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity, iSup_typein_limit, Field.Emb.Cardinal.deg_lt_aleph0, range_familyOfBFamily, CategoryTheory.MorphismProperty.HasSmallObjectArgument.exists_cardinal, 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, isEmpty_toType_iff, CategoryTheory.SmallCategoryCardinalLT.exists_equivalence, sup_typein_limit, Cardinal.mk_Iio_toType_ord_lt, CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.preservesColimit, toType_empty_iff_eq_zero, typein_le_typein', CategoryTheory.SmallObject.prop_iterationFunctor_map_succ, Field.Emb.Cardinal.iSup_filtration, 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 | 171 mathmath: isPrincipal_add_iff_add_self_lt, principal_add_omega, cof_iSup_add_one_le, add_absorp, card_add_one, add_succ, exists_lt_mul, isPrincipal_add_iff_zero_or_omega0_opow, dvd_add_iff, add_right_cancel, existsAddOfLE, ONote.nf_repr_split', cof_add_one, deriv_add_eq_mul_omega0_add, instAddRightMono, isPrincipal_add_ord, CNF.eval_single_add', add_le_iff_of_isSuccLimit, principal_add_of_le_one, CNF.coeff_opow_mul_add, principal_add_ord, lt_mul_div_add, add_log_le_log_mul, isPrincipal_add_one, sSup_add_one_lt_of_lt_cof, le_add_left, opow_add, div_add_mod, mul_add_div, isSuccLimit_add_iff_of_isSuccLimit, nfp_mul_opow_omega0_add, one_add_ofNat, ZFSet.vonNeumann_add_one, opow_mul_add_pos, lift_cof_iSup_add_one, NONote.repr_add, bddAbove_range_add_one_iff, iSup_add_one_lt_of_lt_cof, 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, isPrincipal_add_of_isPrincipal_mul, OrdinalApprox.gfpApprox_add_one, le_sub_of_le, lt_mul_add_one_iff, cof_add, lt_add_iff, ONote.repr_add, IsFundamentalSeq.add_one, derivFamily_add_one, lt_add_iff_of_isSuccLimit, Cardinal.cof_preOmega_add_one, iSup_add_natCast, add_sub_cancel, isPrincipal_add_iff_add_lt_ne_self, sub_lt_of_le, isPrincipal_add_opow_of_isPrincipal_add, card_add, add_eq_zero_iff, mul_succ, veblenWith_add_one, instAddLeftReflectLT, opow_mul_add_lt_opow_mul, sub_le, instAddLeftStrictMono, cof_iSup_Iio_add_one, principal_add_iff_zero_or_omega0_opow, OrdinalApprox.lfpApprox_add_one, principal_add_iff_add_lt_ne_self, principal_add_mul_of_principal_add, principal_add_of_principal_mul, natCast_add_of_omega0_le, one_add_natCast, lift_iSup_add_one_lt_of_lt_cof, CNF.eval_add, isPrincipal_add_omega0, veblen_add_one, Cardinal.preBeth_add_one, ONote.repr_opow_aux₁, sSup_le_sSup_add_one, log_opow_mul_add, lift_add, add_eq_right_iff_mul_omega0_le, mul_add_div_mul, ONote.split_add_lt, bsup_id_add_one, exists_lt_add_of_not_isPrincipal_add, Cardinal.preAleph_add_one, nfp_add_eq_mul_omega0, mul_add_mod_self, lt_iSup_add_one, isPrincipal_add_omega, leftDistribClass, cof_lift_iSup_add_one_le, Cardinal.beth_add_one, IsInitial.isPrincipal_add, CNF.foldr, Cardinal.succ_preAleph, isPrincipal_add_iff_add_left_eq_self, exists_lt_add_of_not_principal_add, principal_add_one, principal_add_omega0, forall_lt_mul, two_opow_log_add, isSuccLimit_add, add_mul_of_isSuccLimit, iSup_add_one_le_iff, instAddLeftReflectLE, iSup_add_one, iSup_Iio_add_one, add_omega0, opow_add_one, add_sub_cancel_of_le, pred_add_one, type_sum_lex, IsInitial.principal_add, Cardinal.beth_eq_preBeth, add_omega0_opow, principal_add_of_principal_mul_opow, add_mul_succ, CNF.opow_mul_add, mul_add_mod_mul, CNF.eval_single_add, add_sub_add_cancel, ONote.repr_opow_aux₂, canonicallyOrderedAdd, Cardinal.aleph_eq_preAleph, le_add_right, Cardinal.isRegular_preAleph_add_one, add_le_iff, isPrincipal_add_mul_of_isPrincipal_add, isNormal_add_right, principal_add_omega0_opow, instAddLeftMono, add_one_eq_succ, add_le_add_iff_right, nfp_add_zero, mul_two, isPrincipal_add_of_le_one, iSup_le_iSup_add_one, iSup_add_one_le, cof_iSup_add_one, add_le_right_iff_mul_omega0_le, isPrincipal_add_omega0_opow, lt_iSup_add_one_iff, isPrincipal_add_of_isPrincipal_mul_opow, principal_add_opow_of_principal_add, lift_add_one, instAddRightReflectLT, ONote.nf_repr_split, IsFundamentalSeq.iSup_add_one_eq, instIsLeftCancelAdd, natCast_add_omega0, deriv_add_one, sub_sub, le_add_sub, bddAbove_add_one_image_iff, Cardinal.cof_omega_add_one, Cardinal.aleph_add_one, omega_eq_preOmega, toZFSet_add_one, Cardinal.isRegular_aleph_add_one, Cardinal.succ_aleph, lt_mul_iff
|
addMonoidWithOne 📖 | CompOp | 91 mathmath: Mathlib.Meta.NormNum.isNat_ordinalMod, lt_omega0_opow_succ, ONote.repr_one, card_le_ofNat, add_right_cancel, ONote.nf_repr_split', succ_one, CNF.eval_single_add', div_two_opow_log, CNF.coeff_opow_mul_add, Cardinal.preAleph_nat, one_add_ofNat, Mathlib.Meta.NormNum.isNat_ordinalNPow, 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, enum_lt_fin, natCast_mod, omega0_le, IsFundamentalSeq.add_one, iSup_add_natCast, card_lt_nat, preOmega_ofNat, Mathlib.Meta.NormNum.isNat_ordinalMul, enum_lt_nat, Cardinal.ord_ofNat, natCast_add_of_omega0_le, one_add_natCast, CNF.eval_add, ONote.repr_opow_aux₁, iSup_mul_natCast, lift_natCast, natCast_pow, natCast_mul, natCast_succ, Mathlib.Meta.NormNum.isNat_ordinalDiv, nsmul_eq_mul, ONote.split_add_lt, natCast_opow_omega0, card_le_nat, type_fintype, lt_omega0_opow, Cardinal.ord_nat, ofNat_lt_card, natCast_lt_omega0, Mathlib.Meta.NormNum.isNat_ordinalSub, ofNat_le_card, card_eq_nat, principal_mul_two, opow_natCast, two_opow_log_add, isInitial_natCast, natCast_mod_omega0, IsNormal.apply_omega0, Mathlib.Meta.NormNum.isNat_ordinalOPow, omega0_opow_mul_nat_lt, nat_lt_omega0, card_nat, ONote.repr_ofNat, isPrincipal_mul_iff_le_two_or_omega0_opow_opow, CNF.eval_single_add, typein_lt_nat, ONote.repr_opow_aux₂, lt_omega0, isPrincipal_mul_two, add_le_add_iff_right, typein_lt_fin, mul_two, card_lt_ofNat, iSup_natCast, lift_ofNat, natCast_lt_epsilon, apply_omega0_of_isNormal, preOmega_natCast, ONote.nf_repr_split, Cardinal.preBeth_nat, lt_omega0_omega0_opow, natCast_lt_of_isSuccLimit, natCast_add_omega0, natCast_lt_gamma, type_fin, principal_mul_iff_le_two_or_omega0_opow_opow, instCharZero, natCast_div, card_eq_ofNat
|
card 📖 | CompOp | 81 mathmath: Cardinal.lt_ord_succ_card, lift_card_iSup_le_sum_card, card_add_one, cof_blsub_le, card_le_ofNat, isInitialIso_apply, card_le_aleph, card_iSup_Iio_le_sum_card, card_one, card_zero, card_typein_min_le_mk, 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, IsInitial.le_ord_iff_card_le, 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, Cardinal.le_ord_iff_card_le_of_lt_aleph0, card_eq_ofNat
|
enum 📖 | CompOp | 22 mathmath: enum_symm_apply_coe, enum_zero_le, enum_lt_enum, enum_le_enum', enum_lt_fin, le_enum_succ, enum_typein, enum_lt_nat, typein_enum, enum_succ_eq_top, not_lt_enum_ord_mk_min_compl, 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 | 132 mathmath: iSup_eq_iSup, iSup_eq_bsup, lift_card_iSup_le_sum_card, Acc.rank_eq, iSup_pow_natCast, cof_iSup_add_one_le, sup_eq_lsub_iff_lt_sup, cof_iSup_le_lift, sInf_compl_lt_lift_ord_succ, max_zero_left, sup_eq_lsub_iff_succ, cof_iSup_Iio, iSup_typein_succ, sup_succ_le_lsub, iSup_le_lsub, card_iSup_Iio_le_sum_card, iSup_lt_of_lt_cof, sSup_add_one_lt_of_lt_cof, card_sInf_range_compl_le_lift, iSup_le, Principal.sSup, lift_cof_iSup_add_one, iSup_pow, deriv_limit, card_sInf_range_compl_le, iSup_add_one_lt_of_lt_cof, sSup_eq_bsup, Cardinal.aleph_add_aleph, iSup_add_nat, iSup_sum, lift_cof_iSup, PSet.rank_insert, iSup_eq_lsub_or_succ_iSup_eq_lsub, sup_succ_eq_lsub, sSup_ord, 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, cof_iSup, opow_limit, cof_iSup_Iio_add_one, Cardinal.ord_eq_iInf, max_eq_zero, bsup_eq_sup, lift_iSup_add_one_lt_of_lt_cof, IsPrincipal.iSup, iSup_mul_natCast, mem_closure_iff_iSup, sSup_le_sSup_add_one, iSup_lt_ord_lift, Cardinal.aleph_max, Cardinal.preAleph_max, mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, iSup'_eq_bsup, lt_iSup_add_one, iSup_sequence_lt_omega_one, cof_lift_iSup_add_one_le, IsWellFounded.rank_eq, iSup_typein_limit, derivFamily_limit, ZFSet.rank_range, iSup_ord, ZFSet.rank_insert, sup_eq_sup, sSup_lt_of_lt_cof, 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, iSup_add_one_le_iff, bsup'_eq_iSup, IsNormal.apply_omega0, iSup_add_one, iSup_Iio_eq_bsup, iSup_Iio_add_one, 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', lift_iSup_lt_of_lt_cof, sup_typein_limit, omega_max, sup_eq_lsub_or_sup_succ_eq_lsub, ZFSet.rank_pair, IsPrincipal.sSup, iSup_le_iSup_add_one, iSup_le_iff, Cardinal.iSup_lt_ord_of_isRegular, iSup_eq_lsub, max_zero_right, iSup_add_one_le, iSup_eq_lsub_iff, cof_iSup_add_one, iSup_natCast, iSup_iterate_eq_nfp, lt_iSup_add_one_iff, apply_omega0_of_isNormal, IsFundamentalSeq.iSup_add_one_eq, lsub_le_sup_succ, succ_iSup_le_lsub_iff, IsNormal.apply_of_isSuccLimit, lsub_sum, iSup_lt_ord, cof_iSup_le, ZFSet.rank_union, preOmega_max, card_iSup_le_sum_card, PSet.rank_pair, IsFundamentalSeq.iSup_eq, sInf_empty, sup_typein_succ, succ_lt_iSup_of_ne_iSup
|
instLinearOrder 📖 | CompOp | 70 mathmath: IsNormal.veblenWith, 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.GoodProducts.linearIndependent_comp_of_eval, 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_veblenWith, 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, CNF.support_coeff, 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, type_lt_ordinal, Profinite.NobelingProof.isClosed_proj, typein_ordinal, Profinite.NobelingProof.swapTrue_mem_C1, cmp_veblenWith, 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.Products.isGood_mono, 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, IsFundamentalSeq.comp_isNormal, Profinite.NobelingProof.Products.eval_πs_image, IsNormal.trans, isNormal_veblenWith_zero, IsNormal.veblenWith_zero, isNormal_omega, Profinite.NobelingProof.succ_mono
|
instOrderBot 📖 | CompOp | 2 mathmath: bot_eq_zero, boundedLimitRec_zero
|
instSuccAddOrder 📖 | CompOp | — |
instSuccOrder 📖 | CompOp | 103 mathmath: 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, type_lt_mem_range_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, 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, ZFSet.rank_powerset, derivFamily_succ, isNormal_iff_lt_succ_and_bsup_eq, lt_opow_succ_log_self, type_lt_mem_range_succ_iff, 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, mul_eq_opow_log_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, 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₂, cof_eq_one_iff, 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, 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, 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 | 128 mathmath: Cardinal.preBeth_omega, lt_omega0_opow_succ, iSup_pow_natCast, isPrincipal_add_iff_zero_or_omega0_opow, invVeblen₂_eq_iff, ONote.nf_repr_split', omega0_lt_omega_one, le_invVeblen₂_iff, deriv_add_eq_mul_omega0_add, omega0_lt_preOmega_iff, opow_omega0, omega_zero, Cardinal.ord_aleph0, isSuccLimit_omega0, epsilon_eq_deriv, isPrincipal_mul_omega0_opow_opow, card_omega0, range_omega, principal_mul_omega0, nfp_mul_opow_omega0_add, principal_opow_omega0, invVeblen₂_le_iff, mul_lt_omega0_opow, card_omega0_opow, natCast_mul_omega0, iSup_pow, ONote.split_dvd, omega0_pos, eq_zero_or_opow_omega0_le_of_mul_eq_right, ONote.NF.of_dvd_omega0, isPrincipal_mul_omega0, 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, nfp_mul_eq_opow_omega0, ONote.repr_scale, omega0_le, iSup_add_natCast, isPrincipal_opow_omega0, 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, isPrincipal_add_omega0, epsilon_succ_eq_nfp, ONote.repr_opow_aux₁, 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, nfp_add_eq_mul_omega0, Cardinal.aleph0_le_preAleph, veblen_invVeblen₁_invVeblen₂, lt_omega0_opow, omega0_lt_epsilon, natCast_lt_omega0, epsilon0_eq_nfp, epsilon_zero_eq_nfp, veblen_mem_range_opow, omega0_le_preOmega_iff, isSuccPrelimit_iff_omega0_dvd, omega0_lt_gamma, deriv_mul_eq_opow_omega0_mul, ONote.NF.of_dvd_omega0_opow, opow_lt_veblen_opow_iff, principal_add_omega0, natCast_mod_omega0, mul_le_right_iff_opow_omega0_dvd, IsNormal.apply_omega0, add_omega0, type_nat_lt, principal_mul_omega0_opow_opow, omega0_opow_mul_nat_lt, nat_lt_omega0, invVeblen₂_lt_iff, Cardinal.beth_eq_preBeth, add_omega0_opow, lift_omega0, isPrincipal_mul_iff_le_two_or_omega0_opow_opow, Cardinal.omega0_lt_ord, ONote.repr_opow_aux₂, Cardinal.aleph_eq_preAleph, invVeblen₂_lt, lt_omega0, lt_invVeblen₂_iff, mul_omega0_opow_opow, 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, isPrincipal_add_omega0_opow, Cardinal.ord_le_omega0, apply_omega0_of_isNormal, Cardinal.ord_eq_omega0, lt_omega0_omega0_opow, mul_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 | 141 mathmath: cof_iSup_add_one_le, card_add_one, opow_one, lift_one, Iio_one_default_eq, omega0_lt_omega_one, succ_one, cof_add_one, Cardinal.lift_eq_aleph_one, div_two_opow_log, card_one, isPrincipal_add_one, Cardinal.aleph0_lt_iff_aleph_one_le, sSup_add_one_lt_of_lt_cof, one_add_ofNat, log_one_left, ZFSet.vonNeumann_add_one, lift_cof_iSup_add_one, div_self, Cardinal.aleph_one_le_continuum, MeasurableSpace.generateMeasurableRec_of_omega_one_le, succ_zero, bddAbove_range_add_one_iff, Cardinal.preBeth_one, zero_opow', cof_one, iSup_add_one_lt_of_lt_cof, one_add_omega0, instZeroLEOneClass, lt_one_iff_zero, one_add_of_omega0_le, opow_one_add, Cardinal.aleph1_le_lift, card_le_one, OrdinalApprox.gfpApprox_add_one, one_lt_pow, cardinalInterFilter_aleph_one_iff, isPrincipal_one_iff, isInitial_one, lt_mul_add_one_iff, Cardinal.ord_eq_one, mod_one, Cardinal.cof_omega_one, Cardinal.beth_one, IsFundamentalSeq.add_one, derivFamily_add_one, Cardinal.cof_preOmega_add_one, bsup_one, Cardinal.aleph1_le_mk_iff, one_lt_card, one_opow, Cardinal.aleph1_lt_lift, Cardinal.lt_aleph_one_iff, type_eq_one_iff_unique, veblenWith_add_one, cof_iSup_Iio_add_one, Cardinal.lift_eq_aleph1, zero_opow_le, OrdinalApprox.lfpApprox_add_one, one_add_natCast, lift_iSup_add_one_lt_of_lt_cof, veblen_add_one, Cardinal.preBeth_add_one, sSup_le_sSup_add_one, omega0_lt_omega1, bsup_id_add_one, Cardinal.preAleph_add_one, lt_iSup_add_one, iSup_sequence_lt_omega_one, Cardinal.aleph_one_le_lift, cof_lift_iSup_add_one_le, Cardinal.beth_add_one, principal_one_iff, Cardinal.lift_le_aleph1, Cardinal.succ_preAleph, CNF.coeff_one_left, Cardinal.ord_one, type_pUnit, principal_add_one, CNF.one_left, card_eq_one, veblenWith_one, Cardinal.aleph0_lt_aleph_one, opow_zero, iSup_add_one_le_iff, Cardinal.isRegular_aleph_one, iSup_add_one, IsFundamentalSequence.succ, iSup_Iio_add_one, Cardinal.lift_le_aleph_one, one_le_iff_ne_zero, opow_add_one, iSup_sequence_lt_omega1, type_unit, one_lt_of_isSuccLimit, type_eq_one_of_unique, pred_add_one, Cardinal.aleph1_eq_lift, MeasurableSpace.generateMeasurableRec_omega_one, blsub_one, typein_one_toType, Cardinal.isRegular_preAleph_add_one, isPrincipal_mul_one, Cardinal.aleph1_le_mk, CountableInterFilter.toCardinalInterFilter, Cardinal.aleph_one_eq_lift, one_lt_opow, Cardinal.countable_iff_lt_aleph_one, nfp_mul_one, add_one_eq_succ, MeasurableSpace.generateMeasurableRec_of_omega1_le, MeasurableSpace.generateMeasurableRec_omega1, Cardinal.aleph_one_le_iff, iSup_le_iSup_add_one, Cardinal.lift_lt_aleph1, iSup_add_one_le, cof_iSup_add_one, Cardinal.aleph_one_lt_lift, lt_iSup_add_one_iff, le_one_iff, lift_add_one, invVeblen₁_epsilon, IsFundamentalSeq.iSup_add_one_eq, principal_mul_one, deriv_add_one, one_lt_omega0, one_le_card, Cardinal.succ_aleph0, bddAbove_add_one_image_iff, Cardinal.cof_omega_add_one, Cardinal.aleph_add_one, div_one, Cardinal.lift_lt_aleph_one, toZFSet_add_one, Cardinal.isRegular_aleph_add_one, ONote.nfBelow_ofNat, instNeZeroOne, one_toType_eq, MeasurableSpace.generateMeasurable_eq_rec, Cardinal.succ_aleph, log_one_right
|
partialOrder 📖 | CompOp | 876 mathmath: isPrincipal_add_iff_add_self_lt, Cardinal.lt_ord_succ_card, isSuccLimit_lift, PSet.rank_le_iff, Cardinal.aleph_le_beth, List.SortedGT.lt_ord_of_lt, opow_le_opow_right, veblenWith_le_veblenWith_iff_right, lt_omega0_opow_succ, isNormal_iff_strictMono_limit, Cardinal.mk_iUnion_Ordinal_le_of_le, principal_add_omega, boundedLimitRec_succ, Acc.rank_eq, sup_eq_lsub_iff_lt_sup, ZFSet.IsOrdinal.rank_le_iff_subset, Profinite.NobelingProof.GoodProducts.sum_to_range, ZFSet.subset_vonNeumann, Cardinal.nfpFamily_lt_ord_of_isRegular, lift_type_lt, sInf_compl_lt_lift_ord_succ, typein_le_typein, pred_succ, mem_range_typein_iff, IsAcc.isSuccLimit, gamma_le_gamma, isPrincipal_iff_of_monotone, add_succ, exists_lt_mul, Cardinal.isStrongLimit_preBeth, Profinite.NobelingProof.injective_πs', card_le_ofNat, Iio_one_default_eq, lsub_pos, Cardinal.blsub_lt_ord_lift_of_isRegular, sup_eq_lsub_iff_succ, Cardinal.aleph_succ, isInitialIso_apply, not_bddAbove_fp_family, blsub_congr, Cardinal.aleph_pos, liftInitialSeg_coe, cof_iSup_Iio, iSup_typein_succ, existsAddOfLE, blsub_le_iff, Cardinal.isSuccLimit_ord, omega_lt_omega, omega0_lt_omega_one, le_invVeblen₂_iff, cof_Iio, type_lt_iff, IsNormal.apply_le_nfp, veblenWith_zero_lt_veblenWith_zero, succ_one, sub_eq_zero_iff_le, Cardinal.ord.orderEmbedding_coe, omega0_lt_preOmega_iff, mulRightMono, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, instAddRightMono, Profinite.NobelingProof.coe_πs, lift_lt, ZFSet.lt_rank_iff, apply_le_nfp, mod_le, Cardinal.lift_eq_aleph_one, add_le_iff_of_isSuccLimit, not_lt_zero, card_le_aleph, isAcc_iff, omega_zero, bsup_id_succ, type_lt_mem_range_succ, liftPrincipalSeg_top', sup_succ_le_lsub, iSup_le_lsub, card_iSup_Iio_le_sum_card, isOpen_singleton_iff, Profinite.NobelingProof.Products.limitOrdinal, enum_symm_apply_coe, IsNormal.lt_iff, 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, mul_div_gc, isInitialIso_symm_apply_coe, isInitial_preOmega, nfp_le_fp, add_log_le_log_mul, Profinite.NobelingProof.Products.eval_πs, card_typein_min_le_mk, Cardinal.aleph0_lt_iff_aleph_one_le, Cardinal.isNormal_preAleph, Cardinal.bddAbove_ord_image_iff, epsilon_zero_lt_gamma, lt_log_of_lt_opow, iSup_lt_of_lt_cof, div_le, sSup_add_one_lt_of_lt_cof, Cardinal.preAleph_nat, lt_mul_iff_div_lt, PSet.rank_mono, Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval, Mathlib.Meta.NormNum.isNat_ordinalLT_true, IsNormal.isSuccLimit, 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, isSuccLimit_add_iff_of_isSuccLimit, cof_preOmega, nfp_mul_opow_omega0_add, div_opow_log_pos, one_add_ofNat, Profinite.NobelingProof.Products.eval_πs', Profinite.NobelingProof.GoodProducts.span_sum, Profinite.NobelingProof.GoodProducts.range_equiv_factorization, isOpen_iff, isSuccLimit_opow_left, iSup_le, Cardinal.ord_pos, le_iff_derivFamily, Cardinal.preAleph_le_aleph, left_lt_opow, CNF.sorted, type_le_iff, opow_mul_add_pos, log_le_self, coe_toZFSet, gamma0_le_of_veblen_le, typein_top, isSuccLimit_opow, invVeblen₂_le_iff, enum_le_enum', apply_lt_nfpFamily_iff, deriv_succ, IsFundamentalSeq.le_ord_cof, bfamilyOfFamily'_typein, invVeblen₁_le, mul_lt_of_lt_div, Cardinal.aleph_one_le_continuum, WellFoundedGT.rank_strictAnti, mul_lt_omega0_opow, Cardinal.bsup_lt_ord_of_isRegular, MeasurableSpace.generateMeasurableRec_of_omega_one_le, Profinite.NobelingProof.succ_exact, veblenWith_right_strictMono, succ_zero, card_le_preAleph, Cardinal.aleph_mul_aleph0, bddAbove_range_add_one_iff, Profinite.NobelingProof.GoodProducts.smaller_factorization, deriv_limit, epsilon_zero_le_of_omega0_opow_le, lt_nfpFamily_iff, omega0_pos, not_bddAbove_principal, veblenWith_zero_strictMono, eq_zero_or_opow_omega0_le_of_mul_eq_right, iSup_add_one_lt_of_lt_cof, nfp_le_of_isPrincipal, Profinite.NobelingProof.πs'_apply_apply, Cardinal.card_le_iff, enumOrd_le_enumOrd, liftPrincipalSeg_coe, Besicovitch.TauPackage.monotone_iUnionUpTo, bsup_le, bsup_succ_eq_blsub, opow_log_le_self, Cardinal.aleph_add_aleph, instZeroLEOneClass, lsub_const, lt_one_iff_zero, isSuccLimit_add_iff, Cardinal.preAleph_omega0, lt_gamma0, foldr_le_nfpFamily, bot_eq_zero, CNF.snd_lt, PSet.rank_lt_of_mem, pred_le_iff_le_succ, Cardinal.beth_succ, mem_range_omega_iff, nat_le_card, IsNormal.limit_lt, mem_toZFSet_iff, right_le_opow, ZFSet.rank_mono, Acc.rank_lt_of_rel, ord_mk_lt_type, Cardinal.lt_omega_iff_card_lt, Cardinal.lsub_lt_ord_of_isRegular, 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, blsub_lt_ord_lift, toZFSet_strictMono, IsAcc.inter_Ioo_nonempty, card_le_one, lt_sub, opow_mul_add_lt_opow, lift_succ, veblen_of_ne_zero, iSup_eq_lsub_or_succ_iSup_eq_lsub, opow_le_opow_iff_right, sup_succ_eq_lsub, type_le_iff', Cardinal.lsub_lt_ord_lift_of_isRegular, div_opow_log_lt, Cardinal.le_aleph_ord, ONote.NFBelow.lt, not_isPrincipal_iff, IsInitial.card_lt_card, typein_lt_typein, eq_nat_or_omega0_le, one_lt_pow, iterate_veblen_lt_gamma0, cardinalInterFilter_aleph_one_iff, nat_lt_card, nfpFamily_lt_ord_lift, IsWellFounded.rank_lt_of_rel, ZFSet.rank_powerset, lt_epsilon_zero, enum_lt_fin, le_sub_of_le, lt_mul_add_one_iff, boundedLimitRec_zero, le_zero, CNF.sortedGT, iterate_omega0_opow_lt_epsilon0, nfpFamily_le_fp, instPosMulStrictMono, derivFamily_succ, IsNormal.id_le, isNormal_iff_lt_succ_and_bsup_eq, Cardinal.aleph_le_aleph, IsNormal.le_apply, lt_add_iff, Cardinal.cof_omega_one, div_le_left, lt_opow_succ_log_self, not_bddAbove_setOf_isPrincipal, Profinite.NobelingProof.contained_eq_proj, IsFundamentalSeq.strictMono, type_lt_mem_range_succ_iff, iterate_le_nfp, IsWellFounded.rank_eq_typein, PSet.rank_sUnion_le, Profinite.NobelingProof.GoodProducts.injective_sum_to, isSuccPrelimit_zero, IsNormal.apply_lt_nfp, le_nfp, omega0_le, bsup_eq_blsub_iff_succ, IsFundamentalSeq.add_one, IsNormal.limit_le, lt_add_iff_of_isSuccLimit, sup_le_lsub, Cardinal.cof_preOmega_add_one, 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, Profinite.NobelingProof.GoodProducts.good_lt_maxProducts, Cardinal.ord_aleph, nfp_lt_ord, small_Iic, Profinite.NobelingProof.GoodProducts.union_succ, isSuccPrelimit_mul_right, Cardinal.aleph1_le_mk_iff, nfp_le_apply, wellFoundedLT, veblenWith_lt_veblenWith_iff, card_lt_nat, ZFSet.mem_vonNeumann', derivFamily_strictMono, blsub_le_of_brange_subset, log_mono_right, ZFSet.vonNeumann_mem_vonNeumann_iff, Profinite.NobelingProof.Products.eval_πs_image', one_lt_card, lt_blsub_iff, Cardinal.ord_le, isNormal_preOmega, sub_lt_of_le, nfpFamily_lt_ord, preOmega_ofNat, preOmega_le_omega, cof_succ, lsub_lt_ord, ZFSet.vonNeumann_strictMono, type_subrel, Cardinal.isRegular_aleph_succ, Cardinal.ord_le_ord, Cardinal.beth_mono, gamma_pos, not_principal_iff_of_monotone, lt_lift_iff, isSuccLimit_of_isPrincipal_add, OrdinalApprox.lfpApprox_monotone, principal_mul_omega, Cardinal.aleph1_lt_lift, Cardinal.lt_aleph_one_iff, le_enum_succ, opow_limit, left_le_veblenWith, OrdinalApprox.gfpApprox_antitone, CNF.eval_lt, Cardinal.preAleph_limit, mem_toPSet_iff, Cardinal.isNormal_aleph, mul_succ, cmp_veblen, ONote.omega0_le_oadd, Cardinal.omega0_le_ord, Order.cof_Iio, enum_typein, instAddLeftReflectLT, opow_mul_add_lt_opow_mul, limitRecOn_succ, sub_le, instAddLeftStrictMono, cof_iSup_Iio_add_one, enum_lt_nat, Cardinal.card_typein_lt, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller, Cardinal.card_typein_toType_lt, blsub_lt_ord, blsub_type, Cardinal.lift_eq_aleph1, zero_opow_le, instOrderTopology, lt_blsub, IsNormal.le_set', bddAbove_range, lift_iSup_add_one_lt_of_lt_cof, accPt_subtype, 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, lt_bsup_of_limit, sSup_le_sSup_add_one, not_principal_iff, iSup_lt_ord_lift, IsNormal.monotone, Cardinal.aleph_max, isSuccLimit_of_principal_add, Cardinal.blsub_lt_ord_of_isRegular, Cardinal.ord_preAleph, omega0_lt_omega1, bfamilyOfFamily_typein, pred_lt_iff_not_isSuccPrelimit, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum, typein_enum, isNormal_iff_lt_succ_and_blsub_eq, Cardinal.isStrongLimit_beth, blsub_le, preOmega_zero, gamma_zero_le_of_veblen_le, aleph0_le_card, typein_surj, isInitial_succ, natCast_succ, coe_preOmega, veblen_zero_le_veblen_zero, Cardinal.preAleph_max, opow_dvd_opow_iff, typein_injective, ord_cof_le, Cardinal.preBeth_le_preBeth, Profinite.NobelingProof.C0_projOrd, toZFSetIso_apply, le_mul_right, bsup_le_of_brange_subset, mem_range_veblen_iff_le_invVeblen₁, add_eq_right_iff_mul_omega0_le, omega0_le_omega, bsup_lt_ord_lift, mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, bsup_eq_blsub_or_succ_bsup_eq_blsub, ONote.split_add_lt, not_isSuccLimit_zero, isSuccLimit_iff, veblen_eq_veblen_iff, pred_eq_iff_isSuccPrelimit, exists_lt_add_of_not_isPrincipal_add, Profinite.NobelingProof.C1_projOrd, mod_opow_log_lt_self, mk_Iio_ordinal, bddAbove_of_small, Profinite.NobelingProof.πs_apply_apply, Cardinal.preAleph_add_one, card_le_nat, typein_apply, lsub_le_of_range_subset, Cardinal.bsup_lt_ord_lift_of_isRegular, ToType.mk_symm_apply_coe, Cardinal.preAleph_le_of_isSuccPrelimit, Cardinal.range_aleph, mul_eq_opow_log_succ, bddAbove_iff_small, Cardinal.beth_limit, Cardinal.aleph0_le_preAleph, IsFundamentalSeq.id, lt_iSup_add_one, Cardinal.preAleph_succ, IsFundamentalSequence.monotone, Profinite.NobelingProof.GoodProducts.square_commutes, strictMono_gamma, Cardinal.derivFamily_lt_ord, IsPrincipal.iterate_lt, enum_succ_eq_top, isPrincipal_add_omega, iterate_veblen_lt_gamma_zero, typein_surjOn, iSup_sequence_lt_omega_one, lt_omega0_opow, enumOrd_le_of_forall_lt, Cardinal.aleph_one_le_lift, IsNormal.eq_iff_zero_and_succ, OrdinalApprox.exists_gfpApprox_eq_gfpApprox, PSet.rank_powerset, blsub_pos, isInitial_omega, epsilon0_lt_gamma, omega0_lt_epsilon, Cardinal.preBeth_succ, Mathlib.Meta.NormNum.isNat_ordinalLE_true, IsWellFounded.rank_eq, iSup_typein_limit, log_eq_iff, Cardinal.not_injective_limitation_set, veblen_le_veblen_iff, bsup_succ_of_mono, bsup_congr, enumOrd_le_of_subset, eq_zero_or_pos, small_Icc, isSuccPrelimit_type_lt_iff, veblen_le_veblen_iff_right, ofNat_lt_card, isSuccLimit_mul, natCast_lt_omega0, Cardinal.lift_le_aleph1, derivFamily_limit, Cardinal.gc_ord_card, ZFSet.rank_range, Profinite.NobelingProof.contained_C1, Cardinal.derivFamily_lt_ord_lift, enumOrd_succ_le, bsup_eq_blsub_iff_lt_bsup, type_lt_ordinal, le_preOmega_self, not_lt_enum_ord_mk_min_compl, isSuccPrelimit_lift, Cardinal.succ_preAleph, WellFoundedLT.rank_strictMono, ZFSet.rank_insert, enum_le_enum, Cardinal.preAleph_zero, lsub_le_iff, lt_opow_iff_log_lt', lt_wf, sSup_lt_of_lt_cof, log_mod_opow_log_lt_log_self, card_succ, Cardinal.IsRegular.cof_omega_eq, sub_le_self, Profinite.NobelingProof.Products.lt_ord_of_lt, aleph0_le_cof, le_iSup, card_omega, Profinite.NobelingProof.isClosed_proj, card_typein, lift_typein_top, Cardinal.IsRegular.ord_pos, typein_ordinal, veblen_lt_veblen_veblen_iff, apply_le_nfpFamily, le_bsup, Cardinal.lift_aleph, div_pos, PSet.rank_singleton, exists_lt_add_of_not_principal_add, ofNat_le_card, omega0_le_preOmega_iff, IsFundamentalSequence.ord_cof, invVeblen₂_le, isSuccPrelimit_iff_omega0_dvd, mulLeftMono, le_sub_of_add_le, instNoMaxOrder, Profinite.NobelingProof.swapTrue_mem_C1, bsup_succ_le_blsub, nfpFamily_monotone, lift_preOmega, succ_iSup_eq_lsub_iff, omega0_lt_gamma, Cardinal.aleph0_le_aleph, zero_lt_card, lift_type_le, IsInitial.card_le_card, le_enumOrd_self, Cardinal.preAleph_le_preAleph, small_Ioc, omega_strictMono, lt_opow_of_log_lt, isPrincipal_mul_omega, lt_pred_iff_succ_lt, div_le_of_le_mul, ONote.fundamentalSequenceProp_inl_some, sup_eq_lsub, veblenWith_le_veblenWith_iff, blsub_succ_of_mono, opow_le_opow, 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, veblenWith_lt_veblenWith_veblenWith_iff, lt_bsup_of_ne_bsup, RelEmbedding.ordinal_type_le, CNF.snd_pos, opow_lt_veblen_opow_iff, nfp_monotone, Cardinal.preBeth_limit, bsup_le_iff, enum_zero_eq_bot, veblenWith_succ, lt_veblen_iff_invVeblen₁_le, Cardinal.nfpFamily_lt_ord_lift_of_isRegular, isSuccLimit_add, Cardinal.preAleph_lt_preAleph, univ_id, gamma_lt_gamma, lt_iSup_iff, Cardinal.aleph_mul_aleph, CNF.lt_snd, Cardinal.beth_strictMono, le_log_of_opow_le, iSup_add_one_le_iff, mul_le_right_iff_opow_omega0_dvd, Cardinal.isRegular_aleph_one, ZFSet.mem_vonNeumann_succ, instAddLeftReflectLE, ZFSet.rank_le_iff, le_lift_iff, iSup_Iio_eq_bsup, IsFundamentalSequence.succ, iSup_Iio_add_one, Profinite.NobelingProof.contained_proj, Cardinal.lift_le_aleph_one, nfpFamily_le_iff, MeasurableSpace.generateMeasurableRec_mono, ONote.repr_le_repr, one_le_iff_ne_zero, veblen_lt_veblen_iff, instIsEmptyIioZero, lt_nfp_iff, ONote.fundamentalSequenceProp_inr, mem_brange, enumOrd_lt_enumOrd, invVeblen₁_lt_iff, ONote.repr_lt_repr, iSup_sequence_lt_omega1, preOmega_strictMono, veblenWith_zero_le_veblenWith_zero, ZFSet.mem_vonNeumann, principal_opow_omega, PSet.lt_rank_iff, card_preOmega, lt_opow_of_isSuccLimit, omega0_opow_mul_nat_lt, epsilon0_le_of_omega0_opow_le, lsub_le_succ_iSup, one_lt_of_isSuccLimit, typein_lt_self, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, lt_veblen, toZFSet_subset_toZFSet_iff, nat_lt_omega0, IsAcc.forall_lt, invVeblen₂_lt_iff, Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim, IsInitial.le_ord_iff_card_le, IsFundamentalSequence.lt, isSuccLimit_of_isPrincipal_mul, Cardinal.aleph1_eq_lift, ZFSet.rank_sUnion_le, nfp_le, lt_mul_iff_of_isSuccLimit, relIso_enum', lt_lsub, bsup_eq_blsub, sInf_compl_lt_ord_succ, Cardinal.ord_strictMono, add_mul_succ, Cardinal.preAleph_le_of_strictMono, Cardinal.preAleph_le_preBeth, MeasurableSpace.generateMeasurableRec_omega_one, Cardinal.ord_lt_ord, blsub_const, bsup_lt_ord, bsup_not_succ_of_ne_bsup, isPrincipal_mul_iff_le_two_or_omega0_opow_opow, ZFSet.rank_lt_of_mem, small_Ioo, Cardinal.preAleph_pos, Cardinal.beth_lt_beth, isSuccLimit_mul_right, ToType.mk_apply, lift_iSup_lt_of_lt_cof, opow_mul_lt_opow, blsub_one, small_Iio, typein_lt_nat, Profinite.NobelingProof.Products.isGood_mono, cof_pos, isSuccPrelimit_mul_left, Profinite.NobelingProof.CC_comp_zero, Cardinal.omega0_lt_ord, typein_one_toType, id_le_enumOrd, succ_pos, apply_lt_nfpFamily, IsFundamentalSeq.comp, opow_lt_opow_iff_right, ONote.repr_opow_aux₂, canonicallyOrderedAdd, bsup_le_blsub, cof_eq_one_iff, toZFSet_monotone, mem_range_preOmega_iff, sup_typein_limit, Profinite.NobelingProof.CC_exact, omega_max, CNF.fst_le_log, mul_le_iff_le_div, Profinite.NobelingProof.Products.prop_of_isGood_of_contained, Cardinal.aleph_eq_preAleph, omega_pos, invVeblen₂_lt, lt_omega0, le_add_right, preOmega_le_of_forall_lt, Cardinal.isRegular_preAleph_add_one, lt_invVeblen₂_iff, add_le_iff, Cardinal.preBeth_strictMono, veblen_right_strictMono, typein_le_typein', succ_pred_eq_iff_not_isSuccPrelimit, Cardinal.aleph1_le_mk, CountableInterFilter.toCardinalInterFilter, Cardinal.aleph_one_eq_lift, one_lt_opow, enum_inj, sup_eq_lsub_or_sup_succ_eq_lsub, Profinite.NobelingProof.injective_πs, Cardinal.aleph_toENat, bddAbove_range_comp, Cardinal.preBeth_mono, Cardinal.countable_iff_lt_aleph_one, veblen_succ, type_Iio_lt, instAddLeftMono, opow_succ, add_one_eq_succ, MeasurableSpace.generateMeasurableRec_of_omega1_le, card_lt_aleph0, nfpFamily_le_apply, IsAcc.pos, IsNormal.le_iff_deriv, lsub_le, Profinite.NobelingProof.coe_πs', omega0_le_of_isSuccLimit, opow_le_iff_le_log, nfpFamily_le, Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective, ZFSet.rank_pair, ZFSet.vonNeumann_of_isSuccPrelimit, add_le_add_iff_right, le_mul_left, MeasurableSpace.generateMeasurableRec_omega1, ZFSet.IsOrdinal.rank_lt_iff_mem, Cardinal.aleph_limit, toZFSet_succ, Cardinal.aleph_one_le_iff, typein_lt_fin, preOmega_le_preOmega, veblenWith_eq_veblenWith_iff, epsilon_pos, opow_lt_opow_left_of_succ, Cardinal.nfp_lt_ord_of_isRegular, sub_lt_of_lt_add, lift_omega, preOmega_omega0, Cardinal.deriv_lt_ord, card_lt_ofNat, iSup_le_iSup_add_one, iSup_le_iff, Cardinal.aleph0_mul_aleph, preOmega_lt_preOmega, left_le_veblen, Cardinal.lift_lt_aleph1, Cardinal.iSup_lt_ord_of_isRegular, Cardinal.ord_card_le, iSup_eq_lsub, not_bddAbove_compl_of_small, log_pos, Cardinal.mk_biUnion_le_of_le, veblen_lt_veblen_iff_right, Principal.iterate_lt, iSup_add_one_le, lt_bsup, iSup_eq_lsub_iff, ZFSet.rank_singleton, add_le_right_iff_mul_omega0_le, iterate_omega0_opow_lt_epsilon_zero, Cardinal.isSuccLimit_omega, isSuccLimit_mul_left, Mathlib.Meta.NormNum.isNat_ordinalLE_false, Cardinal.ord_le_omega0, cof_omega, self_le_succ_pred, Cardinal.aleph_one_lt_lift, typein_inj, lt_iSup_add_one_iff, veblenWith_of_ne_zero, isSuccPrelimit_type_lt, sub_ne_zero_iff_lt, le_one_iff, natCast_lt_epsilon, InitialSeg.ordinal_type_le, instAddRightReflectLT, familyOfBFamily'_enum, bddAbove_image, Cardinal.mk_iUnion_Ordinal_lift_le_of_le, lt_veblen_invVeblen₁, preOmega_natCast, blsub_le_bsup_succ, Cardinal.preBeth_pos, IsNormal.le_iff_eq, enum_zero_le', isSuccLimit_of_principal_mul, toZFSetIso_symm_apply, Cardinal.ord_le_type, isSuccLimit_of_mem_frontier, lsub_unique, lt_omega0_omega0_opow, familyOfBFamily_enum, opow_pos, IsFundamentalSeq.iSup_add_one_eq, opow_le_of_le_log, Cardinal.mem_range_aleph_iff, lsub_le_sup_succ, Cardinal.ord_mono, Cardinal.aleph_lt_aleph, List.Sorted.lt_ord_of_lt, Cardinal.mk_biUnion_le_of_le_lift, IsFundamentalSeq.isCofinal_range, ZFSet.vonNeumann_succ, isPrincipal_opow_omega, succ_iSup_le_lsub_iff, toZFSet_mem_toZFSet_iff, IsFundamentalSeq.comp_isNormal, le_div, nfp_le_of_principal, IsNormal.le_set, veblenWith_pos, natCast_lt_of_isSuccLimit, IsNormal.apply_of_isSuccLimit, IsFundamentalSequence.strict_mono, principal_iff_of_monotone, small_Ico, iSup_lt_ord, Profinite.NobelingProof.Products.eval_πs_image, IsInitial.mem_range_preOmega, Cardinal.lt_ord, nhds_eq_pure, lsub_lt_ord_lift, Cardinal.aleph_toNat, range_preOmega, opow_le_iff_le_log', opow_le_opow_left, one_lt_omega0, preOmega_max, one_le_card, veblen_zero_strictMono, le_add_sub, right_le_veblen, Cardinal.succ_aleph0, opow_le_of_isSuccLimit, iterate_lt_nfp, Cardinal.le_ord_iff_card_le_of_lt_aleph0, ZFSet.le_succ_rank_sUnion, relIso_enum, le_iff_deriv, natCast_lt_gamma, Profinite.NobelingProof.GoodProducts.union, PSet.rank_pair, le_omega_self, Cardinal.aleph_zero, lift_le, bddAbove_add_one_image_iff, isSuccLimit_iff_omega0_dvd, gamma_succ_eq_nfp, enumOrd_strictMono, left_le_opow, lt_lsub_iff, veblenWith_left_monotone, eq_enumOrd, ONote.NFBelow.repr_lt, le_of_dvd, Cardinal.cof_omega_add_one, le_nfpFamily, principal_mul_iff_le_two_or_omega0_opow_opow, IsFundamentalSeq.iSup_eq, lt_epsilon0, Cardinal.aleph_add_one, veblen_pos, Cardinal.lift_preAleph, omega_eq_preOmega, Cardinal.lift_lt_aleph_one, monotone_gamma, Cardinal.isRegular_aleph_add_one, mul_div_le, top_typein, lt_opow_iff_log_lt, isSuccLimit_sub, Profinite.NobelingProof.Products.head_lt_ord_of_isGood, sup_typein_succ, mul_le_iff_of_isSuccLimit, liftPrincipalSeg_top, enum_type, right_le_veblenWith, one_toType_eq, isNormal_omega, Cardinal.isRegular_preAleph_succ, not_isPrincipal_iff_of_monotone, one_lt_cof_iff, MeasurableSpace.generateMeasurable_eq_rec, Profinite.NobelingProof.succ_mono, apply_lt_veblenWith_apply_iff, Cardinal.succ_aleph, succ_lt_iSup_of_ne_iSup, lt_mul_iff, ord_mk_le_type, veblen_left_monotone
|
principalSegToType 📖 | CompOp | — |
termTypeLT_ 📖 | CompOp | — |
termω 📖 | CompOp | — |
toType 📖 | CompOp | — |
toTypeOrderBot 📖 | CompOp | — |
type 📖 | CompOp | 95 mathmath: type_eq, lift_type_lt, mem_range_typein_iff, type_uLift, liftOnWellOrder_type, type_lt_iff, type_lt_mem_range_succ, liftPrincipalSeg_top', enum_symm_apply_coe, blsub_eq_blsub, enum_zero_le, enum_lt_enum, type_ulift, type_lt_ulift, cof_type, type_le_iff, typein_top, brange_bfamilyOfFamily', enum_le_enum', lift_type_eq, type_eq_zero_of_empty, ord_mk_lt_type, typein_lt_type, type_le_iff', enum_lt_fin, type_lt_mem_range_succ_iff, RelIso.ordinal_lift_type_eq, PrincipalSeg.ordinal_type_lt, type_lt_cardinal, Cardinal.ord_eq_Inf, type_subrel, cof_eq', le_enum_succ, type_eq_one_iff_unique, enum_typein, enum_lt_nat, Cardinal.ord_eq_iInf, blsub_type, type_pEmpty, bsup_eq_sup, typein_enum, type_prod_lex, Cardinal.type_cardinal, type_fintype, enum_succ_eq_top, typein_surjOn, isSuccPrelimit_type_lt_iff, type_lt_ordinal, not_lt_enum_ord_mk_min_compl, 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, Cardinal.exists_ord_eq, RelIso.ordinal_type_eq, type_eq_one_of_unique, relIso_enum', type_sum_lex, bsup_eq_sup', Cardinal.ord_eq, ToType.mk_apply, cof_type_lt, blsub_eq_lsub, enum_inj, type_Iio_lt, blsub_eq_lsub', Cardinal.exists_ord_eq_type_lt, bsup_eq_bsup, isSuccPrelimit_type_lt, type_eq_zero_iff_isEmpty, InitialSeg.ordinal_type_le, familyOfBFamily'_enum, enum_zero_le', Cardinal.ord_le_type, familyOfBFamily_enum, type_toType, relIso_enum, type_fin, top_typein, enum_type, one_toType_eq, type_preimage, ord_mk_le_type
|
typein 📖 | CompOp | 40 mathmath: List.SortedGT.lt_ord_of_lt, typein_le_typein, mem_range_typein_iff, iSup_typein_succ, enum_symm_apply_coe, card_typein_min_le_mk, typein_top, bfamilyOfFamily'_typein, typein_lt_type, typein_lt_typein, IsWellFounded.rank_eq_typein, type_subrel, Order.cof_Iio, 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_lt_nat, typein_one_toType, sup_typein_limit, typein_le_typein', type_Iio_lt, typein_lt_fin, typein_inj, List.Sorted.lt_ord_of_lt, top_typein, sup_typein_succ
|
uniqueIioOne 📖 | CompOp | 1 mathmath: Iio_one_default_eq
|
uniqueToTypeOne 📖 | CompOp | — |
univ 📖 | CompOp | 10 mathmath: Cardinal.ord_univ, type_lt_cardinal, cof_univ, Cardinal.type_cardinal, type_lt_ordinal, univ_id, univ_umax, card_univ, lift_univ, liftPrincipalSeg_top
|
wellFoundedRelation 📖 | CompOp | — |
zero 📖 | CompOp | 205 mathmath: CNF.coeff_injective, sub_zero, isPrincipal_add_iff_zero_or_omega0_opow, max_zero_left, Iio_one_default_eq, lsub_pos, instIsLeftCancelMulZero, Cardinal.preBeth_eq_zero, ONote.NFBelow_zero, noZeroDivisors, cof_zero, log_of_left_le_one, veblenWith_zero_lt_veblenWith_zero, sub_eq_zero_iff_le, mod_self, CNF.coeff_zero_left, ZFSet.rank_empty, CNF.eval_single_add', not_lt_zero, gamma_zero_eq_nfp, invVeblen₂_zero, omega_zero, CNF.coeff_opow_mul_add, enum_zero_le, card_zero, invVeblen₁_zero, epsilon_zero_lt_gamma, CNF.coeff_eq_zero_of_lt, log_zero_right, log_zero_left, log_eq_zero, veblen_gamma_zero, div_opow_log_pos, isPrincipal_zero, CNF.zero_left, log_one_left, left_eq_zero_of_add_eq_zero, Cardinal.ord_pos, Cardinal.ord_eq_zero, limitRecOn_zero, opow_mul_add_pos, gamma0_le_of_veblen_le, CNF.coeff_zero_apply, succ_zero, mem_closure_iff_bsup, epsilon_zero_le_of_omega0_opow_le, zero_opow', omega0_pos, zero_sub, veblenWith_zero_strictMono, eq_zero_or_opow_omega0_le_of_mul_eq_right, CNF.coeff_of_not_mem_CNF, IsFundamentalSeq.zero, instZeroLEOneClass, lt_one_iff_zero, isSuccLimit_add_iff, lt_gamma0, Profinite.NobelingProof.GoodProducts.P0, bot_eq_zero, type_eq_zero_of_empty, CNF.of_lt, mul_mod, veblen_zero_lt_veblen_zero, CNF.coeff_of_mem_CNF, enumOrd_zero, iterate_veblen_lt_gamma0, CNF.eval_single, isPrincipal_one_iff, lt_epsilon_zero, veblenWith_zero_inj, 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, bsup_zero, nfp_zero, mem_closed_iff_bsup, Cardinal.ord_zero, div_eq_zero_of_lt, Cardinal.beth_zero, invVeblen₂_gamma, veblen_zero, gamma_pos, add_eq_zero_iff, dvd_iff_mod_eq_zero, principal_add_iff_zero_or_omega0_opow, zero_opow_le, type_pEmpty, max_eq_zero, CNF.eval_add, CNF.support_coeff, CNF.of_le_one, CNF.coeff_of_notMem_CNF, ZFSet.vonNeumann_zero, preOmega_zero, gamma_zero_le_of_veblen_le, PSet.rank_empty, veblen_zero_le_veblen_zero, isNormal_veblen_zero, CNF.rec_zero, mem_closure_tfae, isInitial_zero, not_isSuccLimit_zero, deriv_zero, pred_zero, iterate_veblen_lt_gamma_zero, IsNormal.eq_iff_zero_and_succ, blsub_pos, epsilon0_lt_gamma, 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, div_pos, CNF.coeff_zero_right, deriv_zero_left, mem_range_gamma, CNF.one_left, zero_lt_card, gamma0_eq_nfp, nfp_zero_left, lt_gamma_zero, CNF.snd_pos, opow_zero, mod_zero, enum_zero_eq_bot, isEmpty_toType_zero, CNF.lt_snd, instIsEmptyIioZero, veblenWith_zero, type_empty, veblenWith_zero_le_veblenWith_zero, derivFamily_zero, epsilon0_le_of_omega0_opow_le, CNF.eval_zero_right, Cardinal.preAleph_pos, CNF.eval_single_add, blsub_one, cof_pos, typein_one_toType, succ_pos, bsup_eq_zero_iff, isEmpty_toType_iff, omega_pos, 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, log_pos, max_zero_right, blsub_zero, lsub_empty, iterate_omega0_opow_lt_epsilon_zero, type_eq_zero_iff_isEmpty, le_one_iff, lsub_eq_zero_iff, zero_opow, Cardinal.preBeth_pos, enum_zero_le', opow_pos, invVeblen₁_eq_iff, veblenWith_pos, veblen_zero_inj, right_eq_zero_of_add_eq_zero, veblen_zero_strictMono, isNormal_veblenWith_zero, CNF.zero_right, IsFundamentalSequence.zero, Cardinal.aleph_zero, gamma_succ_eq_nfp, principal_zero, zero_mod, lt_epsilon0, veblen_pos, IsNormal.veblenWith_zero, div_zero, instNeZeroOne, sInf_empty, opow_eq_zero, one_toType_eq, log_one_right
|