| Metric | Count |
|---|
Definitionspred, succ, PredOrder, ofCore, ofLePredIff, ofLinearWellFoundedGT, ofOrderIso, pred, predOrder, succOrder, ofCore, ofLinearWellFoundedLT, ofOrderIso, ofSuccLeIff, succ, instPredOrder, instSuccOrder, instPredOrder, instSuccOrder, instPredOrderOrderDualOfSuccOrder, instSuccOrderOrderDualOfPredOrder | 21 |
Theoremspred_eq, succ_eq, of_succ_le, succ_eq, succ_le, le_pred, of_le_pred, pred_eq, le_pred, succ_le, Icc_pred_left, Icc_pred_right, Icc_pred_right_of_not_isMin, Icc_subset_Ico_succ_right, Icc_subset_Ico_succ_right_of_not_isMax, Icc_subset_Ioc_pred_left, Icc_subset_Ioc_pred_left_of_not_isMin, Icc_succ_left, Icc_succ_left_of_not_isMax, Icc_succ_right, Ici_pred, Ici_subset_Ioi_pred, Ici_subset_Ioi_pred_of_not_isMin, Ici_succ, Ici_succ_of_not_isMax, Ico_pred_left, Ico_pred_right_eq_insert, Ico_subset_Ioo_pred_left, Ico_subset_Ioo_pred_left_of_not_isMin, Ico_succ_left, Ico_succ_left_of_not_isMax, Ico_succ_right, Ico_succ_right_eq_insert, Ico_succ_right_eq_insert_of_not_isMax, Ico_succ_right_of_not_isMax, Iic_pred, Iic_pred_of_not_isMin, Iic_subset_Iio_succ, Iic_subset_Iio_succ_of_not_isMax, Iic_succ, Iio_succ, Iio_succ_eq_insert, Iio_succ_eq_insert_of_not_isMax, Iio_succ_of_not_isMax, Ioc_pred_left, Ioc_pred_left_of_not_isMin, Ioc_pred_right, Ioc_pred_right_of_not_isMin, Ioc_subset_Ioo_succ_right, Ioc_subset_Ioo_succ_right_of_not_isMax, Ioc_succ_right, Ioi_pred, Ioi_pred_eq_insert, Ioi_pred_eq_insert_of_not_isMin, Ioi_pred_of_not_isMin, Ioo_eq_empty_iff_le_succ, Ioo_eq_empty_iff_pred_le, Ioo_pred_left, Ioo_pred_left_of_not_isMin, Ioo_pred_right_eq_insert, Ioo_succ_right, Ioo_succ_right_eq_insert, Ioo_succ_right_eq_insert_of_not_isMax, Ioo_succ_right_of_not_isMax, bot_lt_succ, covBy_succ, covBy_succ_of_not_isMax, gc_pred_succ, instSubsingletonPredOrder, instSubsingletonSuccOrder, isMax_iterate_succ_of_eq_of_lt, isMax_iterate_succ_of_eq_of_ne, isMin_iterate_pred_of_eq_of_lt, isMin_iterate_pred_of_eq_of_ne, le_and_le_succ_iff, le_and_pred_le_iff, le_iff_eq_or_le_pred, le_iff_eq_or_le_pred', le_iff_eq_or_succ_le, le_iff_eq_or_succ_le', le_le_succ_iff, le_of_lt_succ, le_of_pred_le_pred, le_of_pred_lt, le_of_succ_le_succ, le_pred_iff, le_pred_iff_eq_bot, le_pred_iff_isMin, le_pred_iff_of_not_isMin, le_pred_of_lt, le_succ, le_succ_and_le_iff, le_succ_bot_iff, le_succ_iff_eq_or_le, le_succ_iff_pred_le, le_succ_iterate, le_succ_of_wcovBy, le_succ_pred, lt_of_pred_lt_pred, lt_of_succ_lt_succ, lt_succ, lt_succ_bot_iff, lt_succ_iff, lt_succ_iff_eq_or_gt, lt_succ_iff_eq_or_lt, lt_succ_iff_eq_or_lt_of_not_isMax, lt_succ_iff_ne_top, lt_succ_iff_not_isMax, lt_succ_iff_of_not_isMax, lt_succ_of_le, lt_succ_of_le_of_not_isMax, lt_succ_of_not_isMax, max_of_succ_le, min_of_le_pred, not_isMax_pred, not_isMin_succ, pred_bot, pred_covBy, pred_covBy_of_not_isMin, pred_eq_csSup, pred_eq_iSup, pred_eq_iff_covBy, pred_eq_iff_isMin, pred_eq_of_covBy, pred_eq_pred_iff, pred_eq_pred_iff_of_not_isMin, pred_eq_sSup, pred_injective, pred_iterate_le, pred_le, pred_le_and_le_iff, pred_le_iff_eq_or_le, pred_le_iff_le_succ, pred_le_le_iff, pred_le_of_wcovBy, pred_le_pred, pred_le_pred_iff, pred_le_pred_iff_of_not_isMin, pred_le_pred_of_le, pred_le_pred_of_not_isMin_of_le, pred_lt, pred_lt_iff, pred_lt_iff_eq_or_gt, pred_lt_iff_eq_or_lt, pred_lt_iff_eq_or_lt_of_not_isMin, pred_lt_iff_ne_bot, pred_lt_iff_not_isMin, pred_lt_iff_of_not_isMin, pred_lt_of_le, pred_lt_of_le_of_not_isMin, pred_lt_of_not_isMin, pred_lt_of_not_isMin_of_le, pred_lt_pred, pred_lt_pred_iff, pred_lt_pred_iff_of_not_isMin, pred_lt_pred_of_not_isMin, pred_lt_top, pred_mono, pred_ne_pred, pred_ne_pred_iff, pred_ne_top, pred_strictMono, pred_succ, pred_succ_iterate_of_not_isMax, pred_succ_le, pred_succ_of_not_isMax, pred_top_le_iff, pred_top_lt_iff, pred_wcovBy, succ_eq_csInf, succ_eq_iInf, succ_eq_iff_covBy, succ_eq_iff_isMax, succ_eq_of_covBy, succ_eq_sInf, succ_eq_succ_iff, succ_eq_succ_iff_of_not_isMax, succ_injective, succ_le_iff, succ_le_iff_eq_top, succ_le_iff_isMax, succ_le_iff_of_not_isMax, succ_le_of_lt, succ_le_succ, succ_le_succ_iff, succ_le_succ_iff_of_not_isMax, succ_lt_succ, succ_lt_succ_iff, succ_lt_succ_iff_of_not_isMax, succ_lt_succ_of_not_isMax, succ_mono, succ_ne_bot, succ_ne_succ, succ_ne_succ_iff, succ_pred, succ_pred_iterate_of_not_isMin, succ_pred_of_not_isMin, succ_strictMono, succ_top, wcovBy_succ, map_pred, map_succ, ext, ext_iff, le_pred_of_lt, min_of_le_pred, ofCore_pred, pred_le, ext, ext_iff, le_succ, max_of_succ_le, ofCore_succ, succ_le_of_lt, le_succ, pred_le, instIsEmptySuccOrderOfNonempty, orderSucc_bot, orderSucc_coe, pred_coe, pred_coe_of_isMin, pred_coe_of_not_isMin, succ_unbot, instIsEmptyPredOrderOfNonempty, orderPred_coe, orderPred_top, pred_untop, succ_coe, succ_coe_of_isMax, succ_coe_of_not_isMax, coe_pred_of_mem, coe_succ_of_mem, isMax_of_succ_notMem, isMin_of_pred_notMem, pred_notMem_iff_isMin, succ_notMem_iff_isMax | 236 |
| Total | 257 |
| Name | Category | Theorems |
|---|
pred π | CompOp | 202 mathmath: isMax_or_mem_range_pred_or_isPredLimit, WithTop.pred_eq_pred, Finset.insert_Ico_left_eq_Ico_pred, PrincipalSeg.map_pred, Set.Ioo_pred_left_eq_Ioc_of_not_isMin, WithTop.pred_untop, pred_covBy_of_not_isMin, WCovBy.pred_le, not_isPredPrelimit_iff, Set.insert_Ico_left_eq_Ico_pred_of_not_isMin, pred_iterate, Fin.orderPred_succ, OrderIso.map_pred, pred_le_pred_of_le, pred_injective, Set.insert_Ioc_pred_right_eq_Ioc, Antitone.pairwise_disjoint_on_Ioc_pred, exists_pred_iterate_iff_le, not_isPredPrelimit_iff', IsPredPrelimit.lt_pred_iff, not_isPredLimit_pred_of_not_isMin, pred_succ_le, CovBy.pred_eq, le_pred_of_lt, InitialSeg.map_pred, Antitone.pairwise_disjoint_on_Ioo_pred, Ici_pred, Icc_subset_Ioc_pred_left_of_not_isMin, pred_mono, le_succ_pred, pred_ofAdd, succ_pred_of_not_isMin, Fin.orderPred_zero, Set.insert_Ico_left_eq_Ico_pred, Finset.Ioi_pred_eq_Ici_of_not_isMin, Finset.Icc_pred_right_eq_Ico_of_not_isMin, pred_min, Set.Ioc_pred_left_eq_Icc_of_not_isMin, Monotone.pairwise_disjoint_on_Ioc_pred, not_isPredPrelimit_pred_of_not_isMin, pred_le_iff_eq_or_le, Finset.insert_Ico_left_eq_Ico_pred_of_not_isMin, pred_toMul, IsPredArchimedean.exists_pred_iterate_of_le, LE.le.exists_pred_iterate, Ioo_pred_left, IsPredArchimedean.pred_findAtom, PredOrder.colimitRecOn_pred_of_not_isMin, Set.Icc_pred_right_eq_Ico, Iic_pred, not_isPredPrelimit_pred, pred_top_le_iff, Ioi_pred, mem_range_pred_or_isPredPrelimit, WithTop.pred_coe, pred_le_of_wcovBy, le_pred_iff_of_not_isMin, pred_lt_pred, WithBot.pred_coe, pred_succ, isPredPrelimitRecOn_pred_of_not_isMin, pred_le_pred_iff, pred_eq_of_covBy, Iic_pred_of_not_isMin, Set.Iic_pred_eq_Iio_of_not_isMin, pred_lt_iff_not_isMin, Set.Icc_succ_pred_eq_Ioo, pred_succ_of_not_isMax, pred_lt_iff_eq_or_lt, Finset.insert_Ioc_pred_right_eq_Ioc, Ioc_pred_left_of_not_isMin, Set.Ioi_pred_eq_Ici_of_not_isMin, Finset.Icc_succ_pred_eq_Ioo, pred_bot, pred_lt_top, LT.lt.le_pred, Set.Ioc_pred_right_eq_Ioo, iterate_pred_toZ, IsPredPrelimit.pred_le_iff, IsPredLimit.lt_pred_iff, Finset.Iic_pred_eq_Iio, toZ_iterate_pred_ge, Nat.pred_eq_pred, WithTop.orderPred_coe, Ioi_pred_eq_insert, Ico_subset_Ioo_pred_left, Fin.orderPred_apply, pred_eq_sSup, Finset.insert_Ioc_left_eq_Ioc_pred_of_not_isMin, pred_eq_pred_iff_of_not_isMin, Set.Ioi_pred_eq_Ici, pred_le_pred_of_not_isMin_of_le, Set.Ioc_pred_left_eq_Icc, pred_eq_sub_one, pred_notMem_iff_isMin, pred_lt_of_le, pred_le_iff_le_succ, Finset.Icc_pred_right_eq_Ico, Ioi_pred_of_not_isMin, Finset.Ioc_pred_right_eq_Ioo, pred_covBy, le_iff_eq_or_le_pred', WithTop.orderPred_top, pred_le_le_iff, WithBot.pred_coe_of_not_isMin, pred_max, Ioc_pred_right, pred_top_lt_iff, Finset.Ioc_pred_pred_eq_Ico, Set.Iic_pred_eq_Iio, mem_range_pred_of_not_isPredPrelimit, Set.Ioc_pred_pred_eq_Ico_of_not_isMin, Icc_pred_right, pred_eq_iSup, isPredLimitRecOn_pred, pred_le, Set.Ioc_pred_pred_eq_Ico, Finset.Ioo_pred_left_eq_Ioc, Finset.Ioi_pred_eq_Ici, pred_iterate_le, Set.Ici.coe_pred_of_not_isMin, pred_strictMono, Finset.insert_Icc_pred_right_eq_Icc, Ici_subset_Ioi_pred_of_not_isMin, Monotone.pairwise_disjoint_on_Ico_pred, pred_eq_csSup, Finset.Iic_pred_eq_Iio_of_not_isMin, Set.Ioo_pred_left_eq_Ioc, pred_lt_iff_ne_bot, pred_lt_pred_of_not_isMin, pred_lt_pred_iff, toZ_iterate_pred, Finset.Ioc_pred_left_eq_Icc_of_not_isMin, Fin.orderPred_eq, IsPredPrelimit.lt_pred, pred_eq_iff_isMin, not_isPredLimit_pred, Monotone.pairwise_disjoint_on_Ioo_pred, Finset.Ioc_pred_left_eq_Icc, isPredLimitRecOn_pred_of_not_isMin, pred_le_pred_iff_of_not_isMin, WithBot.pred_coe_of_isMin, exists_pred_iterate_or, pred_eq_iff_covBy, le_pred_iff_eq_bot, Int.pred_eq_pred, le_pred_iff_isMin, Set.Ici.pred_eq_of_not_isMin, Ioc_pred_right_of_not_isMin, pred_le_pred, Ioi_pred_eq_insert_of_not_isMin, Ioo_pred_right_eq_insert, isPredPrelimitRecOn_pred, pred_eq_pred_iff, Finset.Ioc_pred_pred_eq_Ico_of_not_isMin, succ_pred, le_succ_iff_pred_le, Finset.insert_Ioc_left_eq_Ioc_pred, pred_toAdd, IsMin.pred_eq, pred_lt_of_le_of_not_isMin, Ici_subset_Ioi_pred, Icc_pred_right_of_not_isMin, Set.Icc_pred_right_eq_Ico_of_not_isMin, pred_lt_of_not_isMin_of_le, IsMin.le_pred, le_iff_eq_or_le_pred, PredOrder.prelimitRecOn_pred_of_not_isMin, IsPredLimit.pred_le_iff, Ioo_eq_empty_iff_pred_le, le_and_pred_le_iff, pred_ofMul, Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin, not_isMax_pred, Antitone.pairwise_disjoint_on_Ico_pred, gc_pred_succ, pred_lt_iff, le_pred_iff, pred_succ_iterate_of_not_isMax, pred_le_and_le_iff, Finset.insert_Ico_pred_right_eq_Ico, Set.insert_Ico_pred_right_eq_Ico, Set.insert_Icc_pred_right_eq_Icc, Finset.Ioo_pred_left_eq_Ioc_of_not_isMin, Set.insert_Ioc_left_eq_Ioc_pred, Icc_subset_Ioc_pred_left, pred_lt_iff_eq_or_gt, isPredPrelimit_iff_lt_pred, PredOrder.prelimitRecOn_pred, Ico_pred_right_eq_insert, Ioc_pred_left, pred_lt_iff_of_not_isMin, toZ_of_lt, pred_lt_iff_eq_or_lt_of_not_isMin, IsPredLimit.lt_pred, pred_lt, Ioo_pred_left_of_not_isMin, pred_lt_of_not_isMin, pred_lt_pred_iff_of_not_isMin, pred_wcovBy, PredOrder.colimitRecOn_pred, Ico_subset_Ioo_pred_left_of_not_isMin
|
succ π | CompOp | 386 mathmath: Finset.insert_Ico_succ_left_eq_Ico, Cardinal.lt_ord_succ_card, Ordinal.succ_nmul, Ordinal.lt_omega0_opow_succ, Ordinal.boundedLimitRec_succ, Finset.Ici_succ_eq_Ioi_of_not_isMax, Acc.rank_eq, Iio_succ_of_not_isMax, Ioo_succ_right, IsSuccLimit.succ_lt_iff, Ordinal.sInf_compl_lt_lift_ord_succ, Ordinal.pred_succ, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map_le_succ, Ordinal.add_succ, partialSups_succ', Ici_succ_of_not_isMax, Ordinal.sup_eq_lsub_iff_succ, Cardinal.aleph_succ, PrincipalSeg.map_succ, Set.Iio_succ_eq_Iic, Iio_succ_eq_insert_of_not_isMax, succ_lt_succ_iff, SuccOrder.limitRecOn_succ, InverseSystem.piEquivSucc_self, Ordinal.iSup_typein_succ, Ico_succ_right_of_not_isMax, CategoryTheory.Functor.WellOrderInductionData.map_succ, succ_toAdd, Ordinal.succ_one, Set.Icc_succ_left_eq_Ioc, Field.Emb.Cardinal.filtration_succ, Set.Iic.succ_eq_of_not_isMax, Finset.Ico_succ_right_eq_Icc_of_not_isMax, iUnion_Ioc_map_succ_eq_Ioi, OrdinalApprox.gfpApprox_ord_mem_fixedPoint, Ordinal.bsup_id_succ, Ordinal.sup_succ_le_lsub, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_self_succ, isSuccLimitRecOn_succ_of_not_isMax, mem_range_succ_or_isSuccPrelimit, Nimber.succ_def, PSet.le_succ_rank_sUnion, Cardinal.succ_eq_of_lt_aleph0, not_isSuccPrelimit_succ_of_not_isMax, Ioo_eq_empty_iff_le_succ, Set.insert_Ico_right_eq_Ico_succ_of_not_isMax, succ_eq_add_one, Cardinal.succ_natCast, succ_lt_succ, le_succ_and_le_iff, pred_succ_le, Set.Ioo_succ_right_eq_Ioc_of_not_isMax, succ_ofAdd, isSuccPrelimit_iff_succ_lt, Ordinal.div_le, exists_succ_iterate_iff_le, Iic_subset_Iio_succ, Icc_succ_left_of_not_isMax, InitialSeg.map_succ, biUnion_Ici_Ico_map_succ, succ_eq_iInf, Ordinal.cof_eq_one_iff_is_succ, Cardinal.lift_succ, Ico_succ_right_eq_insert, le_iff_eq_or_succ_le, le_succ_pred, Ordinal.lt_mul_succ_div, Ordinal.nfp_mul_opow_omega0_add, succ_pred_of_not_isMin, Ordinal.one_add_ofNat, Finset.Icc_succ_left_eq_Ioc_of_not_isMax, Set.Ico_succ_right_eq_Icc_of_not_isMax, Ordinal.iSup_succ, InverseSystem.globalEquiv_compatibility, IsNormal.ext, Ordinal.deriv_succ, Iio_succ_eq_insert, NatOrdinal.succ_def, lt_succ_iff_eq_or_gt, Field.Emb.Cardinal.succEquiv_coherence, Ordinal.succ_zero, Antitone.pairwise_disjoint_on_Ioo_succ, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality_assoc, succ_top, Set.Ico_succ_succ_eq_Ioc, le_and_le_succ_iff, CategoryTheory.OrthogonalReflection.iteration_map_succ, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_succ_eq, lt_succ_iff_eq_or_lt, Cardinal.card_le_iff, Ordinal.bsup_succ_eq_blsub, Ordinal.lsub_const, Ordinal.nmul_succ, isMin_or_mem_range_succ_or_isSuccLimit, Ordinal.pred_le_iff_le_succ, Cardinal.beth_succ, Ici_succ, le_succ_of_wcovBy, CategoryTheory.SmallObject.SuccStruct.extendToSucc.map_eq, succ_min, succ_pred_iterate_of_not_isMin, CategoryTheory.SmallObject.SuccStruct.extendToSuccObjIso_hom_naturality, PSet.rank_insert, WithBot.succ_coe, Ordinal.lift_succ, Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub, Set.insert_Ioc_succ_left_eq_Ioc, succ_strictMono, Ordinal.sup_succ_eq_lsub, Ordinal.succ_log_def, succ_ofMul, succ_iterate, Ioo_succ_right_eq_insert_of_not_isMax, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_hom_app, ZFSet.rank_powerset, pred_succ, OrderIso.map_succ, Finset.Iio_succ_eq_Iic_of_not_isMax, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, succ_le_iff_of_not_isMax, not_isSuccPrelimit_iff', Ordinal.derivFamily_succ, Ordinal.isNormal_iff_lt_succ_and_bsup_eq, Set.Icc_succ_pred_eq_Ioo, pred_succ_of_not_isMax, succ_le_of_lt, Ordinal.lt_opow_succ_log_self, IsMax.succ_le, Finset.insert_Ioc_succ_left_eq_Ioc, Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax, succ_lt_succ_of_not_isMax, partialSups_succ, Ordinal.bsup_eq_blsub_iff_succ, Ioc_subset_Ioo_succ_right_of_not_isMax, Nat.succ_eq_succ, Set.insert_Ico_right_eq_Ico_succ, Set.insert_Icc_succ_left_eq_Icc, Set.insert_Ico_succ_left_eq_Ico, Ordinal.zero_or_succ_or_isSuccLimit, OrdinalApprox.lfpApprox_ord_eq_lfp, lt_succ_of_not_isMax, Finset.Icc_succ_pred_eq_Ioo, Ioc_subset_Ioo_succ_right, SuccOrder.prelimitRecOn_succ_of_not_isMax, Finset.Ioo_succ_right_eq_Ioc, lt_succ_of_le, succ_eq_iff_isMax, succ_le_iff_isMax, Finset.insert_Ioc_right_eq_Ioc_succ, Finset.Ioo_succ_right_eq_Ioc_of_not_isMax, toZ_of_ge, Field.Emb.Cardinal.equivSucc_coherence, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ_assoc, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, isSuccLimitRecOn_succ, Ordinal.cof_succ, Cardinal.isRegular_aleph_succ, IsSuccPrelimit.le_succ_iff, Ico_succ_right, CategoryTheory.SmallObject.ΞΉFunctorObj_eq, CovBy.succ_eq, Ordinal.le_enum_succ, Cardinal.isRegular_succ, Ordinal.mul_succ, not_isMin_succ, Ordinal.limitRecOn_succ, lt_succ, WCovBy.le_succ, Antitone.pairwise_disjoint_on_Ioc_succ, Cardinal.add_one_le_succ, Set.Icc_succ_left_eq_Ioc_of_not_isMax, Finset.Ici_succ_eq_Ioi, Finset.Iio_succ_eq_Iic, transfiniteIterate_succ, Iio_succ, Ordinal.one_add_natCast, OrdinalApprox.gfpApprox_ord_eq_gfp, succ_le_succ_iff_of_not_isMax, LE.le.exists_succ_iterate, pred_le_iff_le_succ, Ordinal.epsilon_succ_eq_nfp, Ordinal.lt_div, IsSuccLimit.succ_lt, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_succ, Set.Ico_succ_left_eq_Ioo, CategoryTheory.SmallObject.SuccStruct.extendToSucc.obj_eq, Ordinal.isNormal_iff_lt_succ_and_blsub_eq, lt_succ_iff_eq_or_lt_of_not_isMax, CategoryTheory.Functor.WellOrderInductionData.Extension.map_succ, WithBot.orderSucc_bot, lt_succ_iff, Ordinal.isInitial_succ, Ordinal.natCast_succ, succ_injective, CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc, Ordinal.bsup_eq_blsub_or_succ_bsup_eq_blsub, WithBot.succ_unbot, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ, CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso_inv_app, Finset.insert_Icc_succ_left_eq_Icc, Ico_succ_left, not_isSuccLimit_succ_of_not_isMax, Ico_succ_right_eq_insert_of_not_isMax, Ioo_succ_right_of_not_isMax, Ordinal.one_nadd, Monotone.disjointed_succ, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq, Ordinal.mul_eq_opow_log_succ, toZ_iterate_succ, Ordinal.opow_mul_add_lt_opow_succ, Cardinal.preAleph_succ, PNat.succ_eq_add_one, Ordinal.enum_succ_eq_top, lt_succ_iff_not_isMax, succ_le_succ_iff, CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity, Fin.orderSucc_last, succ_toMul, Ordinal.IsNormal.eq_iff_zero_and_succ, OrdinalApprox.exists_gfpApprox_eq_gfpApprox, PSet.rank_powerset, Cardinal.preBeth_succ, Cardinal.nat_succ, IsWellFounded.rank_eq, Ordinal.log_eq_iff, Ordinal.bsup_succ_of_mono, Set.Iio_succ_eq_Iic_of_not_isMax, Finset.Icc_succ_left_eq_Ioc, IsSuccPrelimit.succ_lt_iff, ZFSet.rank_range, Ordinal.enumOrd_succ_le, Cardinal.succ_def, succ_mono, Fin.orderSucc_apply, Monotone.pairwise_disjoint_on_Ioo_succ, ZFSet.rank_insert, succ_eq_succ_iff, Ordinal.card_succ, succ_notMem_iff_isMax, CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_left, PSet.rank_singleton, succ_lt_succ_iff_of_not_isMax, CategoryTheory.SmallObject.ΟFunctorObj_eq, iSup_succ, Ordinal.bsup_succ_le_blsub, Ordinal.succ_iSup_eq_lsub_iff, SuccOrder.limitRecOn_succ_of_not_isMax, succ_le_succ, Ioo_succ_right_eq_insert, Ordinal.lt_pred_iff_succ_lt, ONote.fundamentalSequenceProp_inl_some, Set.Ioo_succ_right_eq_Ioc, Monotone.pairwise_disjoint_on_Ioc_succ, Ordinal.sup_eq_lsub, Ordinal.blsub_succ_of_mono, Set.Iic.coe_succ_of_not_isMax, Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax, Ico_succ_left_of_not_isMax, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem, CategoryTheory.SmallObject.SuccStruct.extendToSucc_map, WithBot.orderSucc_coe, Ordinal.veblenWith_succ, toZ_iterate_succ_le, isSuccPrelimitRecOn_succ_of_not_isMax, ZFSet.mem_vonNeumann_succ, IsSuccPrelimit.succ_lt, IsSuccArchimedean.exists_succ_iterate_of_le, Ordinal.IsFundamentalSequence.succ, disjointed_succ, succ_le_iff, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_succ_eq, Ordinal.nadd_succ, Finset.insert_Ico_right_eq_Ico_succ, Ordinal.lsub_le_succ_iSup, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, succ_eq_csInf, succ_eq_succ_iff_of_not_isMax, Cardinal.powerlt_succ, Monotone.disjointed_succ_sup, succ_pred, le_succ_iff_pred_le, Set.Ico_succ_right_eq_Icc, CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc, lt_succ_iff_of_not_isMax, Ordinal.bsup_eq_blsub, SuccOrder.prelimitRecOn_succ, Ordinal.sInf_compl_lt_ord_succ, Ordinal.add_mul_succ, le_iff_eq_or_succ_le', Set.Ici_succ_eq_Ioi, lt_succ_of_le_of_not_isMax, Ordinal.blsub_const, Ordinal.bsup_not_succ_of_ne_bsup, covBy_succ, Ordinal.blsub_one, Cardinal.succ_zero, succ_eq_of_covBy, Ordinal.succ_pos, le_succ, WithTop.succ_coe_of_isMax, Finset.Ico_succ_succ_eq_Ioc_of_not_isMax, ONote.repr_opow_auxβ, iUnion_Ico_map_succ_eq_Ici, LT.lt.succ_le, ENat.succ_def, Finset.Ico_succ_left_eq_Ioo, le_succ_bot_iff, IsSuccLimit.le_succ_iff, wcovBy_succ, Ordinal.succ_pred_eq_iff_not_isSuccPrelimit, Fin.orderSucc_castSucc, Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub, not_isSuccPrelimit_succ, Ordinal.veblen_succ, CategoryTheory.SmallObject.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.SuccStruct.arrowSucc_def, Ordinal.opow_succ, succ_eq_iff_covBy, gc_pred_succ, Ordinal.add_one_eq_succ, WithTop.succ_coe, lt_succ_bot_iff, ZFSet.rank_pair, Set.Ici_succ_eq_Ioi_of_not_isMax, Ordinal.opow_mul_add_lt_opow_mul_succ, Ordinal.toZFSet_succ, Ordinal.opow_lt_opow_left_of_succ, Icc_succ_left, Ordinal.iSup_eq_lsub, CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity, IsMax.succ_eq, Monotone.biUnion_Ico_Ioc_map_succ, Ordinal.iSup_eq_lsub_iff, CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp, le_le_succ_iff, Iic_succ, ZFSet.rank_singleton, Int.succ_eq_succ, Ordinal.self_le_succ_pred, iterate_succ_toZ, WithBot.succ_eq_succ, covBy_succ_of_not_isMax, Finset.insert_Ico_right_eq_Ico_succ_of_not_isMax, Fin.orderSucc_eq, Iic_subset_Iio_succ_of_not_isMax, mem_range_succ_of_not_isSuccPrelimit, Ordinal.blsub_le_bsup_succ, Icc_subset_Ico_succ_right_of_not_isMax, Ordinal.lsub_unique, lt_succ_iff_ne_top, Set.insert_Ioc_right_eq_Ioc_succ, CategoryTheory.SmallObject.SuccStruct.Iteration.prop_map_succ, exists_succ_iterate_or, Ordinal.lsub_le_sup_succ, succ_le_iff_eq_top, succ_max, biUnion_Ici_Ioc_map_succ, ZFSet.vonNeumann_succ, Ordinal.succ_iSup_le_lsub_iff, Finset.Ico_succ_succ_eq_Ioc, Cardinal.succ_pos, Ordinal.succ_nadd, not_isSuccPrelimit_iff, Set.Ico_succ_succ_eq_Ioc_of_not_isMax, WithTop.succ_coe_of_not_isMax, Ordinal.nadd_one, bot_lt_succ, Cardinal.succ_aleph0, ZFSet.le_succ_rank_sUnion, le_succ_iff_eq_or_le, CategoryTheory.SmallObject.SuccStruct.arrowMap_extendToSucc, PSet.rank_pair, Icc_subset_Ico_succ_right, Ordinal.gamma_succ_eq_nfp, le_succ_iterate, isSuccPrelimitRecOn_succ, succ_eq_sInf, Finset.Ico_succ_right_eq_Icc, Ordinal.sup_typein_succ, Antitone.pairwise_disjoint_on_Ico_succ, not_isSuccLimit_succ, Cardinal.isRegular_preAleph_succ, Ordinal.succ_lt_iSup_of_ne_iSup, Monotone.pairwise_disjoint_on_Ico_succ
|