`OAI/SetTheory/PartitionPrinciple/Transfinite/`

3225 declarations, 0 contain sorry, 0 declared as axioms; 208 files

Files

AgreementLimits.lean 3 declarations
AmalgamationCoinitiality.lean 7 declarations
AttachmentCoinitiality.lean 7 declarations
ChronologicalTheorem.lean 23 declarations
CodedMainPrefixSystems.lean 49 declarations
CoherentTower.lean 38 declarations
CoinitialityPreservation.lean 5 declarations
CompressionPrefixCoinitiality.lean 20 declarations
CountableCoding.lean 7 declarations
CrossStageParameterSupports.lean 1 declarations
ExternalBirthLayerSeparation.lean 20 declarations
ExternalChronologyStageLaws.lean 62 declarations
ExternalRequestRankBounds.lean 6 declarations
FairPreparationBirthPersistence.lean 1 declarations
FinalCardinality.lean 35 declarations
FinalInsertionStages.lean 3 declarations
FinalRectangleStages.lean 2 declarations
FinalStageBounds.lean 26 declarations
FiniteFamilyRankBounds.lean 4 declarations
FiniteFlatHistoryCoherence.lean 27 declarations
GluingBirthRanges.lean 68 declarations
GroundBatchBirths.lean 38 declarations
GroundBinaryRowStageOneRefinement.lean 8 declarations
GroundCanonicalCompressionHistory.lean 7 declarations
GroundChronologicalBasis.lean 13 declarations
GroundChronologicalCompressionCoinitiality.lean 2 declarations
GroundChronologicalExternalCoinitiality.lean 2 declarations
GroundChronologyFieldAppend.lean 35 declarations
GroundChronologyLayerRelation.lean 6 declarations
GroundChronologyPairRanks.lean 6 declarations
GroundChronologyPairs.lean 13 declarations
GroundCoinitialOperations.lean 25 declarations
GroundCompressionBirthData.lean 31 declarations
GroundCompressionBirths.lean 7 declarations
GroundCompressionCarrierRankBounds.lean 3 declarations
GroundCompressionPrefixGraphs.lean 24 declarations
GroundCountableFunctionClosure.lean 35 declarations
GroundCountableFunctionEnumerations.lean 1 declarations
GroundCountableFunctionOrdinaryZFC.lean 2 declarations
GroundCountableFunctionSequences.lean 2 declarations
GroundCountableFunctionZF.lean 1 declarations
GroundCountableLayerCodes.lean 6 declarations
GroundCountableProducts.lean 10 declarations
GroundCountableRelationSelections.lean 10 declarations
GroundCountableRowExactUnions.lean 1 declarations
GroundCountableRowSequenceReflection.lean 2 declarations
GroundDefinableRefinementHistories.lean 6 declarations
GroundExtensionOrdinals.lean 5 declarations
GroundExternalBirthLayers.lean 19 declarations
GroundExternalSerializedChronology.lean 11 declarations
GroundFairPreparationLimitCertificates.lean 3 declarations
GroundFiniteBirthHistories.lean 4 declarations
GroundFixedFairPreparationLimitCertificates.lean 1 declarations
GroundFlatLimitAdequacy.lean 3 declarations
GroundFlatSuccessorAssignmentGraphs.lean 14 declarations
GroundFlatSuccessorAtomicTransfer.lean 2 declarations
GroundFlatSuccessorProjectedFilters.lean 4 declarations
GroundFourFlatStageHistories.lean 27 declarations
GroundHistoryFields.lean 2 declarations
GroundHistoryUnionBounds.lean 13 declarations
GroundInaccessibleOrdinalClosure.lean 2 declarations
GroundInitialCompressionHistory.lean 29 declarations
GroundInitialCompressionPrefix.lean 1 declarations
GroundInitialExternalBirths.lean 1 declarations
GroundInitialExternalChronology.lean 21 declarations
GroundInitialMainSeedSuccessorSerialization.lean 25 declarations
GroundInitialMainStage.lean 39 declarations
GroundInitialPreservedMainPrefix.lean 27 declarations
GroundInitialRecursiveSuccessor.lean 1 declarations
GroundIntervalRecursion.lean 8 declarations
GroundInvariantSuccessors.lean 24 declarations
GroundLayerBirthFibers.lean 6 declarations
GroundLinkedMainStageCodeLaws.lean 37 declarations
GroundLinkedMainStageLevels.lean 11 declarations
GroundMainFinalChronology.lean 8 declarations
GroundMainFinalPersistentSuccessorLabels.lean 1 declarations
GroundMainFinalPrefixCompatibleCaps.lean 1 declarations
GroundMainFinalPrefixPreparationBatches.lean 1 declarations
GroundMainFinalPreparedPrefixBounds.lean 1 declarations
GroundMainFinalStageOneClosure.lean 4 declarations
GroundMainFinalStageThreeClosure.lean 3 declarations
GroundMainFinalStageThreeHistory.lean 4 declarations
GroundMainFinalStageThreeSupport.lean 5 declarations
GroundMainFinalStageTwoClosure.lean 2 declarations
GroundMainFinalStageTwoIndices.lean 8 declarations
GroundMainFinalStageTwoSupport.lean 1 declarations
GroundMainFinalStructuralPrefixDescent.lean 1 declarations
GroundMainFinalStructuralSizeFamilies.lean 2 declarations
GroundMainFinalSuccessorPreparedProfiles.lean 1 declarations
GroundMainOrdinalConstructionData.lean 3 declarations
GroundMainPrefixConePreservation.lean 51 declarations
GroundMainPrefixConeValues.lean 17 declarations
GroundMainPrefixCoveredLimitAppend.lean 3 declarations
GroundMainPrefixDecoding.lean 42 declarations
GroundMainPrefixExtensionRelations.lean 4 declarations
GroundMainPrefixFieldFamilies.lean 27 declarations
GroundMainPrefixFinalDirectedness.lean 1 declarations
GroundMainPrefixFinalInsertion.lean 15 declarations
GroundMainPrefixFinalStrictGrowth.lean 10 declarations
GroundMainPrefixInsertionSuccessors.lean 1 declarations
GroundMainPrefixLimitBottom.lean 57 declarations
GroundMainPrefixLimitChronologyCore.lean 52 declarations
GroundMainPrefixLimitCoverageConstruction.lean 46 declarations
GroundMainPrefixLimitCoverageGraph.lean 99 declarations
GroundMainPrefixLimitGroupLaws.lean 85 declarations
GroundMainPrefixLimitSizes.lean 6 declarations
GroundMainPrefixOmegaOneAppend.lean 1 declarations
GroundMainPrefixPreservedSeeds.lean 30 declarations
GroundMainPrefixPriorFields.lean 17 declarations
GroundMainPrefixRawCoveredAppend.lean 15 declarations
GroundMainPrefixRectangleLocalization.lean 3 declarations
GroundMainPrefixSelectedStepTotality.lean 18 declarations
GroundMainPrefixSelectedSuccessors.lean 1 declarations
GroundMainPrefixSuccessor.lean 1 declarations
GroundMainPrefixTopColumns.lean 36 declarations
GroundMainStageCandidates.lean 25 declarations
GroundMainStageFromCodes.lean 40 declarations
GroundMainStageInvariant.lean 11 declarations
GroundMainSuccessorCompressionActors.lean 3 declarations
GroundMainSuccessorProfilePreservation.lean 22 declarations
GroundMainSuccessorSeparation.lean 3 declarations
GroundNaturalRecursion.lean 5 declarations
GroundOmegaOneTaskBearingSuccessorFunction.lean 13 declarations
GroundOrdinalEnumerationFamilies.lean 7 declarations
GroundOrdinalImagePartitions.lean 6 declarations
GroundOrdinalOrderCodes.lean 20 declarations
GroundOrdinalPartialMapCovers.lean 1 declarations
GroundOrdinaryCountableFunctions.lean 2 declarations
GroundRankedSerializedChronology.lean 1 declarations
GroundRawFinitePowerStageSystems.lean 1 declarations
GroundRawRefinementStageZF.lean 2 declarations
GroundRecursiveOriginalRowFamilies.lean 2 declarations
GroundRecursiveRefinementBinaryUnions.lean 21 declarations
GroundRecursiveRefinementInternalClosure.lean 2 declarations
GroundRecursiveRefinementMixedUnions.lean 2 declarations
GroundRecursiveRowCompleteProjection.lean 38 declarations
GroundRefinementFullIndexSize.lean 2 declarations
GroundRefinementHistorySpliceSteps.lean 3 declarations
GroundSelectedMainLimitCoverage.lean 3 declarations
GroundSerializedChronologyRestrictions.lean 7 declarations
GroundSerializedChronologyTimeEquality.lean 49 declarations
GroundSerializedCompressionChronology.lean 2 declarations
GroundSmallAssignmentCuts.lean 1 declarations
GroundSmallFamilyRangeRanks.lean 1 declarations
GroundSmallFunctionSpaces.lean 5 declarations
GroundStageOneAssignmentImages.lean 6 declarations
GroundStageOneAssignmentUnions.lean 36 declarations
GroundStageOneOrder.lean 6 declarations
GroundStageOneProjectedFilters.lean 13 declarations
GroundStageOneSequenceProjections.lean 15 declarations
GroundStageOneTestEquivalence.lean 8 declarations
GroundStageThreeAssignmentFamilies.lean 25 declarations
GroundStageThreeClosureData.lean 6 declarations
GroundStageThreeInternalClosure.lean 14 declarations
GroundStageThreeSuccessorLaws.lean 35 declarations
GroundStageTwoAtomicLifting.lean 2 declarations
GroundStageTwoIndexAnchors.lean 3 declarations
GroundStageTwoProjectedFilters.lean 4 declarations
GroundStageTwoRefinementObjects.lean 4 declarations
GroundStandardInaccessible.lean 26 declarations
GroundStrongLimitPowers.lean 3 declarations
GroundStructuralBirthLevelSelectors.lean 1 declarations
GroundStructuralFullIndexSize.lean 17 declarations
GroundStructuralFullIndexWeakSize.lean 3 declarations
GroundStructuralHistoryTestUnions.lean 33 declarations
GroundStructuralRefinementHistories.lean 6 declarations
GroundTaskBearingSuccessorDecoding.lean 32 declarations
GroundTwoStageMainDiagram.lean 45 declarations
HeightTower.lean 18 declarations
InaccessibleBounds.lean 20 declarations
InitialRecursiveTaskLaws.lean 5 declarations
LimitGroup.lean 23 declarations
LimitProfilePersistence.lean 16 declarations
LinkedSuccessorOutputFieldEquality.lean 31 declarations
MainBirthExtensions.lean 64 declarations
MainBirthOrigins.lean 45 declarations
MainOrdinalSteps.lean 14 declarations
MainPrefixHistoryUnionRecognition.lean 65 declarations
MainPrefixSelectedTraceLaws.lean 23 declarations
MainStageFilterBases.lean 10 declarations
MainStageTaskCodes.lean 7 declarations
NaturalRecursionTraceValues.lean 2 declarations
NonzeroLimitOrdinalCodes.lean 21 declarations
OrdinalExternalHeights.lean 18 declarations
OrdinalRecursionTraces.lean 26 declarations
OrdinalSetCodes.lean 6 declarations
OwnerBirthLayers.lean 19 declarations
PartialBatchLimits.lean 9 declarations
PreservedMainPrefixHistoryValues.lean 2 declarations
RecursiveLiftAgreement.lean 65 declarations
RecursiveMaps.lean 34 declarations
RecursiveNextMapInputs.lean 9 declarations
RecursiveRefinementInclusionCoherence.lean 1 declarations
RecursiveRefinementMapCoherence.lean 4 declarations
RecursiveStateFieldEnvironments.lean 40 declarations
RecursiveStructuralRefinementHistories.lean 2 declarations
RefinementBirthEnumerationFairness.lean 26 declarations
RefinementBirthSchedules.lean 2 declarations
RefinementFlatSuccessorUnions.lean 2 declarations
RefinementHistoryPrefixLevels.lean 36 declarations
SerializedChronologyCodes.lean 6 declarations
SetRankBounds.lean 6 declarations
SmallTileHeightInputs.lean 11 declarations
StageOneDataBoundLaws.lean 33 declarations
StageTwoAssignmentSplices.lean 14 declarations
StageTwoClosureData.lean 23 declarations
StageTwoSupportData.lean 10 declarations
SuccessorBirths.lean 80 declarations