`OAI/SetTheory/PartitionPrinciple/Geometry/`

3783 declarations, 0 contain sorry, 0 declared as axioms; 271 files

Files

AssignmentIndexLevels.lean 4 declarations
AssignmentNestedSplices.lean 21 declarations
AtomicEqualitySteps.lean 8 declarations
AtomicSoundness.lean 2 declarations
BinaryTiles.lean 42 declarations
CheckCertificates.lean 5 declarations
CompatibleCopies.lean 21 declarations
CompleteProjectionPredensity.lean 16 declarations
Compression.lean 121 declarations
CompressionExternalTileOverlaps.lean 56 declarations
CompressionTheorem.lean 3 declarations
CompressionUnionBaseFilling.lean 24 declarations
DecodedGroundGroups.lean 17 declarations
DecodedMeetMaps.lean 14 declarations
DepthLayerHeights.lean 5 declarations
DirectSystem.lean 21 declarations
EligibleBatchAgreement.lean 3 declarations
EligibleTaskCovariance.lean 12 declarations
ExternalColumnOrders.lean 4 declarations
ExternalCopyDescent.lean 10 declarations
ExternalHeights.lean 17 declarations
ExternalOwnerCoordinateLaws.lean 26 declarations
ExternalTileVertexPresentation.lean 4 declarations
ExternalTranslation.lean 51 declarations
FinalProfilePersistence.lean 24 declarations
FinalRectangles.lean 2 declarations
FiniteIntervalExtension.lean 2 declarations
FiniteIterationTraces.lean 8 declarations
FiniteWordOperations.lean 10 declarations
FixedCompressionSeeds.lean 1 declarations
GluingHeights.lean 97 declarations
GroundAbsentLiftRangeCollisions.lean 10 declarations
GroundAssignmentIndexLevels.lean 11 declarations
GroundAssignmentLabelDomainTotality.lean 2 declarations
GroundAssignmentRepresentativeClosure.lean 8 declarations
GroundAssignmentRequestBatches.lean 4 declarations
GroundAttachmentEmbeddings.lean 28 declarations
GroundBatchAttachment.lean 16 declarations
GroundBatchEmbeddingRecognition.lean 28 declarations
GroundBatchHeightGraphs.lean 6 declarations
GroundBelowExternalPoints.lean 11 declarations
GroundBelowFamilies.lean 6 declarations
GroundBelowInitialCompression.lean 19 declarations
GroundBinaryRowRecordedPreparationBounds.lean 8 declarations
GroundBinaryRows.lean 7 declarations
GroundBinaryUnionFamilies.lean 5 declarations
GroundCantorDiagonal.lean 6 declarations
GroundCertificateBasisUnions.lean 6 declarations
GroundCertificateProfileImageFamilies.lean 26 declarations
GroundCodedBinaryHeights.lean 32 declarations
GroundCoherentHeightUnion.lean 6 declarations
GroundCompleteProjectionRefinementTests.lean 1 declarations
GroundCompletedCompressionCertificateRecognition.lean 4 declarations
GroundCompletedMapRecognition.lean 6 declarations
GroundCompressionFiniteFieldGraphs.lean 4 declarations
GroundCompressionHeightSteps.lean 55 declarations
GroundCompressionMarkingRecognition.lean 8 declarations
GroundCompressionOrigins.lean 29 declarations
GroundCompressionStampBounds.lean 39 declarations
GroundCompressionStarIncidence.lean 61 declarations
GroundConstantBatchLayers.lean 14 declarations
GroundContainmentOrders.lean 15 declarations
GroundCumulativeHierarchyLevels.lean 23 declarations
GroundDefinableIndexBounds.lean 4 declarations
GroundDefinableRowAssignmentOrders.lean 8 declarations
GroundDefinableSelections.lean 8 declarations
GroundEligibleCaps.lean 34 declarations
GroundEqualityStep.lean 2 declarations
GroundExternalAlphabetInversion.lean 13 declarations
GroundExternalCompressionFieldRecognition.lean 6 declarations
GroundExternalCutoffCoherence.lean 9 declarations
GroundExternalCutoffLayers.lean 1 declarations
GroundExternalGenerators.lean 38 declarations
GroundExternalGroupEmbeddings.lean 9 declarations
GroundExternalLocalHeightFamilies.lean 17 declarations
GroundExternalLocalHeightSelection.lean 39 declarations
GroundExternalMainTransition.lean 7 declarations
GroundExternalProfilePreservation.lean 20 declarations
GroundExternalRawPriorLayers.lean 3 declarations
GroundExternalRectangleFulfillment.lean 2 declarations
GroundExternalRequestFieldRecognition.lean 9 declarations
GroundExternalRequestOverlaps.lean 8 declarations
GroundExternalRewriteSteps.lean 9 declarations
GroundExternalSerializedCore.lean 7 declarations
GroundExternalSlotCopies.lean 6 declarations
GroundExternalStarOverlaps.lean 30 declarations
GroundExternalTileSlotSupports.lean 26 declarations
GroundFairPreparationEventOrigins.lean 2 declarations
GroundFairPreparationMonotonicity.lean 26 declarations
GroundFairRefinementAssignmentVisits.lean 4 declarations
GroundFamilyValueUnions.lean 6 declarations
GroundFinalInsertionExceptions.lean 30 declarations
GroundFiniteAccounting.lean 4 declarations
GroundFiniteSeedBounds.lean 3 declarations
GroundFiniteWordLaws.lean 47 declarations
GroundFiniteWordLength.lean 7 declarations
GroundFixedTopOrders.lean 5 declarations
GroundForcedSequenceReadings.lean 1 declarations
GroundGeometry.lean 6 declarations
GroundGrowthLayerRecognition.lean 9 declarations
GroundHartogs.lean 6 declarations
GroundHeightPushforward.lean 21 declarations
GroundIdentityInsertionTasks.lean 15 declarations
GroundIndexedClassInclusions.lean 22 declarations
GroundIndexedImageCovers.lean 3 declarations
GroundIndexedMixedOperationLifts.lean 3 declarations
GroundIndexedOperationLifts.lean 6 declarations
GroundIndexedSubstructures.lean 2 declarations
GroundIndexedValueLifts.lean 2 declarations
GroundInitialCompletedCompressionCertificates.lean 29 declarations
GroundInitialCompressionCompletion.lean 7 declarations
GroundInitialCompressionIterates.lean 1 declarations
GroundInitialCompressionOrigin.lean 15 declarations
GroundInitialExternalGroup.lean 8 declarations
GroundInitialExternalHeights.lean 5 declarations
GroundInitialLiftEmbeddings.lean 1 declarations
GroundInitialMainAlgebra.lean 1 declarations
GroundInitialSeedMatchedSerialization.lean 1 declarations
GroundInitialSeedSerializationRanks.lean 11 declarations
GroundInternalNoChooserConsequences.lean 2 declarations
GroundInternalRowsInZF.lean 4 declarations
GroundIntervalEmbeddingRelation.lean 5 declarations
GroundIntervalSelection.lean 10 declarations
GroundLayerSourceCongruence.lean 4 declarations
GroundLiftedCompressionGraphs.lean 3 declarations
GroundLinkedProfilePreservation.lean 6 declarations
GroundLinkedProfileTransitionRecognition.lean 3 declarations
GroundLinkedTransitionRetarget.lean 13 declarations
GroundLiteralTaskFieldRecognition.lean 11 declarations
GroundMainBoundTaskOutput.lean 24 declarations
GroundMainCompressionActorCode.lean 4 declarations
GroundMainDiagramAppend.lean 12 declarations
GroundMainFinalDecidedVisibility.lean 1 declarations
GroundMainFinalEnumeratedCertificateFamilies.lean 2 declarations
GroundMainFinalExtensionBases.lean 1 declarations
GroundMainFinalFairPreparationOrbits.lean 4 declarations
GroundMainFinalFulfillmentConstruction.lean 4 declarations
GroundMainFinalOrdinaryInsertion.lean 5 declarations
GroundMainFinalPersistentAssignmentLabels.lean 4 declarations
GroundMainFinalPreparedInsertionProfiles.lean 2 declarations
GroundMainFinalRefinementSystem.lean 1 declarations
GroundMainFinalRowModelDescent.lean 4 declarations
GroundMainFinalRowOrdinaryZF.lean 9 declarations
GroundMainFinalRowOrdinaryZFC.lean 1 declarations
GroundMainFinalRowRectangles.lean 8 declarations
GroundMainFinalRowTerms.lean 15 declarations
GroundMainFinalSeparatedActors.lean 19 declarations
GroundMainFinalStoredPreparedDensity.lean 1 declarations
GroundMainFinalStructuralCompression.lean 11 declarations
GroundMainFinalStructuralLateProfileExclusions.lean 1 declarations
GroundMainFinalStructuralRectangleRefinements.lean 4 declarations
GroundMainFinalStructuralRefinementOutputs.lean 2 declarations
GroundMainFinalStructuralRowNoChooser.lean 1 declarations
GroundMainFinalStructuralSeparationRefinements.lean 1 declarations
GroundMainTaskCapFulfillment.lean 22 declarations
GroundMainTransitionLaws.lean 12 declarations
GroundMainTransitionValidity.lean 8 declarations
GroundMeetGeneratorSteps.lean 6 declarations
GroundMixtureDensityRecovery.lean 16 declarations
GroundMixtureTermBounds.lean 8 declarations
GroundNaturalFamilyShift.lean 25 declarations
GroundNaturalNumbers.lean 3 declarations
GroundNiceAssignmentClassFamilies.lean 3 declarations
GroundNiceRefinementVisibility.lean 32 declarations
GroundNormalizedRefinementOutputs.lean 5 declarations
GroundOmegaOneRowModel.lean 7 declarations
GroundOrdinarySubmodelReflection.lean 14 declarations
GroundPartialCoverPartitions.lean 6 declarations
GroundPredenseMeet.lean 1 declarations
GroundPreparationFamilyImages.lean 34 declarations
GroundPreparedAlignedReferenceCollisions.lean 9 declarations
GroundPreparedMixedCollisions.lean 6 declarations
GroundPreparedPositionCollisions.lean 10 declarations
GroundPreparedSelectionProfiles.lean 2 declarations
GroundPreparedStructuralInsertionCollisions.lean 4 declarations
GroundPresentedPreimages.lean 2 declarations
GroundProfiledExternalRequests.lean 15 declarations
GroundProjectedRowUniqueFibers.lean 3 declarations
GroundRankedCompressionSerialization.lean 1 declarations
GroundRankedExternalSerialization.lean 1 declarations
GroundRankedLayerSelection.lean 2 declarations
GroundRawCandidateDensity.lean 2 declarations
GroundRawLayerPushforward.lean 11 declarations
GroundRawRefinementDataIdentification.lean 7 declarations
GroundRecognizedInitialOrigin.lean 3 declarations
GroundRefinementAbsentLiftInsertions.lean 2 declarations
GroundRefinementAssignmentImages.lean 7 declarations
GroundRefinementAssignmentLabelEntries.lean 2 declarations
GroundRefinementCoarseVisibility.lean 4 declarations
GroundRefinementDataOutputs.lean 4 declarations
GroundRefinementFinitePowerSystems.lean 1 declarations
GroundRefinementRawTestMonotonicity.lean 16 declarations
GroundRefinementVisibleLiftInsertions.lean 11 declarations
GroundRepresentativeIndexSteps.lean 4 declarations
GroundRequestedCompressionTiles.lean 8 declarations
GroundRequestedRectangleHeights.lean 47 declarations
GroundRetainedPreparationSelections.lean 7 declarations
GroundRowAssignmentCuts.lean 7 declarations
GroundRowAssignmentProjections.lean 9 declarations
GroundRowAssignmentTransitionFamilies.lean 5 declarations
GroundRowDistinguishing.lean 17 declarations
GroundSerialOrbits.lean 1 declarations
GroundSerializedBoundNormalization.lean 7 declarations
GroundSerializedCandidateLevels.lean 16 declarations
GroundSharedRefinementValidity.lean 4 declarations
GroundSingleAttachment.lean 59 declarations
GroundStoredPreparationFamilyPersistence.lean 3 declarations
GroundStoredVisitCertificates.lean 3 declarations
GroundStructuralCompleteProjections.lean 2 declarations
GroundStructuralFinitePowerTerms.lean 1 declarations
GroundTaskBearingInsertionFulfillment.lean 11 declarations
GroundTaskBearingRectangles.lean 2 declarations
GroundTaskBearingSeparation.lean 2 declarations
GroundTaskBearingStrictTop.lean 2 declarations
GroundTaskRepresentativeRecognition.lean 15 declarations
GroundTemplateHeightRanges.lean 5 declarations
GroundTemplateIntervalFamilies.lean 35 declarations
GroundTileStarIncidence.lean 33 declarations
GroundTwoPointHeights.lean 8 declarations
GroundUnionInterpretation.lean 4 declarations
GroundVisibilitySupportIncidence.lean 10 declarations
GrowthLayerSourceCongruence.lean 5 declarations
HeightAttachment.lean 12 declarations
HeightColumnBoundLaws.lean 7 declarations
InitialCompressionAccounting.lean 15 declarations
InitialCompressionUnionProfiles.lean 16 declarations
InitialRepresentativeAgreement.lean 3 declarations
IntervalEmbeddingFamilyCodes.lean 40 declarations
IntervalTraceValidity.lean 1 declarations
LiftedCompressionEmbeddings.lean 8 declarations
LiftedCompressionFunctions.lean 12 declarations
MainDiagramGluing.lean 18 declarations
MainDiagrams.lean 43 declarations
MainEndpoints.lean 17 declarations
MainInitial.lean 8 declarations
MainInsertion.lean 12 declarations
MainProfilePersistence.lean 6 declarations
MainRectangleMeets.lean 23 declarations
MainRectangles.lean 14 declarations
NodeCoding.lean 75 declarations
OldProfilePreservationComposition.lean 5 declarations
OutwardSchedule.lean 43 declarations
PartialBatchStep.lean 25 declarations
PresentedRowAssignmentDecoding.lean 4 declarations
PresentedRowAssignmentTotality.lean 1 declarations
PrincipalBatch.lean 150 declarations
RationalHeightDescent.lean 4 declarations
RationalOrderBounds.lean 37 declarations
RawEqualitySteps.lean 8 declarations
RectangleFulfillmentAtBound.lean 48 declarations
RectangleTile.lean 38 declarations
RefinementIndexThreeLevels.lean 7 declarations
RefinementLevelThreeTestGuards.lean 2 declarations
RefinementLevelThreeUnionGuards.lean 1 declarations
RefinementValidityReindex.lean 2 declarations
RepresentativeIndexSteps.lean 43 declarations
RequestedOwnerSlotLaws.lean 24 declarations
RootedSupportOrder.lean 6 declarations
RowAssignmentOrderLaws.lean 2 declarations
RowAssignmentTransitionFamilies.lean 5 declarations
RowAtomicDescent.lean 3 declarations
RowCopyRefinements.lean 17 declarations
RowPositionBounds.lean 19 declarations
SeparationTileCodes.lean 68 declarations
StructuralPreparationSourceImages.lean 34 declarations
TaggedGrowthLayerRanks.lean 4 declarations
TaskSystem.lean 37 declarations
TemplateHeightRangeCodes.lean 32 declarations
TileStarIncomingCodes.lean 62 declarations
TileTreeGluing.lean 58 declarations
UniformAtomicEquality.lean 24 declarations