`OAI/SetTheory/PartitionPrinciple/Definability/`

2526 declarations, 0 contain sorry, 0 declared as axioms; 217 files

Files

AssignmentQueryFormulas.lean 11 declarations
AttachmentOldCodeLaws.lean 3 declarations
BatchAttachmentRealization.lean 46 declarations
BatchGraphSetFormulas.lean 17 declarations
BoundedAtomicEquality.lean 12 declarations
BoundedChronologyCodes.lean 6 declarations
BoundedDirectedOrders.lean 4 declarations
BoundedMeetOrderCodes.lean 3 declarations
BoundedRelationImageEquality.lean 2 declarations
CodedBatchDecoding.lean 7 declarations
CodedEqualityRelations.lean 7 declarations
CodedFilterImages.lean 8 declarations
CodedInjectiveCones.lean 47 declarations
CodedLayerRestrictions.lean 2 declarations
CodedLayerSourceCongruence.lean 1 declarations
CodedProfileImageTests.lean 2 declarations
CodedRangeCompletion.lean 3 declarations
CodedTemplateShadowLaws.lean 7 declarations
CompressionExternalStepRealization.lean 45 declarations
CompressionRequestRealization.lean 13 declarations
CountableFormulaFamilies.lean 4 declarations
CountableSetFormulas.lean 42 declarations
CrossStageMembershipFormulas.lean 2 declarations
DecodedFunctionGraphs.lean 6 declarations
DepthSlotCodes.lean 23 declarations
EqualityStepSyntax.lean 10 declarations
EquivalenceClassCodes.lean 15 declarations
ExternalColumnCodes.lean 11 declarations
ExternalCopyRelations.lean 15 declarations
ExternalFamilySlotCodes.lean 1 declarations
ExternalGroupOperationGraphs.lean 14 declarations
ExternalRealization.lean 12 declarations
ExternalRequestGraphCoordinates.lean 4 declarations
ExternalSlotCopyGraphs.lean 5 declarations
ExternalStarCarrierRanks.lean 9 declarations
ExternalStarOverlapRealization.lean 7 declarations
ExternalTileCoordinateRealization.lean 6 declarations
ExternalTileSlotSupportRealization.lean 6 declarations
ExternalWordRewriteFormulas.lean 17 declarations
ExternalWordRewriteRealization.lean 3 declarations
ExternalWordRewriteRelations.lean 33 declarations
FinalRankRealization.lean 6 declarations
FiniteWordMapCodes.lean 15 declarations
FiniteWordOperationFormulas.lean 4 declarations
FixedTopCodes.lean 40 declarations
FlatCopyGraphRealization.lean 5 declarations
FlatLimitConditionFormulas.lean 10 declarations
ForcingHistoryConditionFormulas.lean 4 declarations
ForcingHistoryOutputFormulas.lean 10 declarations
ForcingWitnessFormulas.lean 2 declarations
FormulaSymmetry.lean 4 declarations
GraphValueMembershipFormula.lean 3 declarations
GreedyAntichainStepFormulas.lean 6 declarations
GroundActedRepresentativeGraphs.lean 11 declarations
GroundAllSupportCodes.lean 3 declarations
GroundAssignmentClassGraphs.lean 15 declarations
GroundBatchAttachmentGraphs.lean 24 declarations
GroundBelowFunctionGraphs.lean 18 declarations
GroundBelowIndexedCarriers.lean 2 declarations
GroundBelowMainGraphs.lean 9 declarations
GroundBelowRelationSpaces.lean 3 declarations
GroundBinaryRowSets.lean 4 declarations
GroundBoundedCompressionHeights.lean 1 declarations
GroundBoundedExternalBirths.lean 18 declarations
GroundCompletedCompressionCertificateFormulas.lean 7 declarations
GroundCompositionFamilyFormulas.lean 4 declarations
GroundCompressionHistoryFormulas.lean 2 declarations
GroundDefinableRelationProducts.lean 8 declarations
GroundDepthSlotCodes.lean 3 declarations
GroundEligibleTaskSetRecognition.lean 4 declarations
GroundExternalCutoffFieldGraphs.lean 5 declarations
GroundExternalRequestSetRecognition.lean 62 declarations
GroundFlatCarrierSequences.lean 5 declarations
GroundFlatCopyGraphs.lean 49 declarations
GroundFlatCopyPresentation.lean 18 declarations
GroundFlatRestrictionGraphs.lean 2 declarations
GroundFunctionCoordinateDensity.lean 5 declarations
GroundFunctionRangeFamilies.lean 12 declarations
GroundInternalRowSetZF.lean 4 declarations
GroundLiftedCompressionFormulas.lean 9 declarations
GroundLiftedRowTupleProvenance.lean 29 declarations
GroundLiftedRowTupleSupports.lean 1 declarations
GroundLowRankFunctionGraphs.lean 3 declarations
GroundMainCodeRanks.lean 6 declarations
GroundMainFinalGraphValueCandidateAvailability.lean 9 declarations
GroundMainFinalSemanticStructuralZF.lean 4 declarations
GroundMainTransitionCodes.lean 1 declarations
GroundNiceVisibilityGraphs.lean 5 declarations
GroundOutsideRowCodes.lean 4 declarations
GroundPackedRefinementFormulaData.lean 38 declarations
GroundPairCompositions.lean 61 declarations
GroundPairEmptyRefinementSystem.lean 1 declarations
GroundPairedCompositionRows.lean 1 declarations
GroundPartialFunctionSpaces.lean 32 declarations
GroundPowerImageGraphs.lean 12 declarations
GroundPreparationEventSupportGraphs.lean 12 declarations
GroundPrincipalNiceSupportCodes.lean 9 declarations
GroundPushFilterFamilyFormulas.lean 9 declarations
GroundQuantifiedGraphFormulas.lean 6 declarations
GroundRankedBoundedSerialization.lean 1 declarations
GroundRationalCodes.lean 45 declarations
GroundRecursiveActionFormulas.lean 12 declarations
GroundRefinementLevelSingleCodes.lean 3 declarations
GroundRefinementLiftedClassGraphs.lean 1 declarations
GroundRefinementPairClassGraphs.lean 45 declarations
GroundRegularFormulas.lean 22 declarations
GroundRelationProductFamilies.lean 5 declarations
GroundRowGraphDescent.lean 1 declarations
GroundSelectedSupportTupleFamilies.lean 28 declarations
GroundSemanticAbsentLiftActors.lean 1 declarations
GroundSemanticAlignedCopyCollisions.lean 6 declarations
GroundSemanticAlignedCopyUnions.lean 5 declarations
GroundSemanticAlignedLargerCutTests.lean 7 declarations
GroundSemanticAlignedRectangleUnions.lean 2 declarations
GroundSemanticAssignmentLabelCanonicalSuccessors.lean 6 declarations
GroundSemanticAssignmentLabelDomainTotality.lean 10 declarations
GroundSemanticAssignmentLabelInjectionPackages.lean 3 declarations
GroundSemanticAugmentedClassRequests.lean 7 declarations
GroundSemanticFairPreparationLimits.lean 7 declarations
GroundSemanticFairPreparationRecordedLimits.lean 7 declarations
GroundSemanticFairPreparationSupportedLimits.lean 1 declarations
GroundSemanticOrdinalRowOrbitCovers.lean 9 declarations
GroundSemanticPreparedProfileSelections.lean 1 declarations
GroundSemanticPreparedWitnessSelections.lean 6 declarations
GroundSemanticRepresentedDomainAbsentLift.lean 4 declarations
GroundSemanticRepresentedDomainEasyCases.lean 7 declarations
GroundSemanticRepresentedDomainLiftDecisions.lean 3 declarations
GroundSemanticRepresentedDomainPersistence.lean 3 declarations
GroundSemanticStructuralCutActions.lean 10 declarations
GroundSemanticStructuralDataSupport.lean 15 declarations
GroundSemanticStructuralFamilyEvaluation.lean 10 declarations
GroundSemanticStructuralFilterLifts.lean 1 declarations
GroundSemanticStructuralFinalRefinements.lean 9 declarations
GroundSemanticStructuralOrderCoordinates.lean 1 declarations
GroundSemanticStructuralPrefixPreparationInputs.lean 5 declarations
GroundSemanticStructuralRefinementNormalization.lean 9 declarations
GroundSemanticStructuralRefinementObjectSupports.lean 1 declarations
GroundSemanticStructuralRequestActions.lean 1 declarations
GroundSemanticStructuralRequestBatches.lean 1 declarations
GroundSemanticStructuralSupportIncidence.lean 1 declarations
GroundSemanticStructuralSymmetricRefinementOutputs.lean 8 declarations
GroundSeparatorFamilyFormulas.lean 5 declarations
GroundSerializedCodeRanks.lean 11 declarations
GroundStageOneFormulaData.lean 2 declarations
GroundStandardInaccessibleFormulas.lean 16 declarations
GroundStrongLimitFormulas.lean 4 declarations
GroundTaggedComponentGraphs.lean 6 declarations
GroundVaryingPreparationRelations.lean 19 declarations
HistoryFieldFormulas.lean 6 declarations
IndexedAttachmentCodes.lean 25 declarations
IndexedMixedOperationLiftCodes.lean 4 declarations
IndexedOperationLiftCodes.lean 8 declarations
IndexedSubstructureCodes.lean 10 declarations
IndexedValueLiftCodes.lean 5 declarations
InitialMainAlgebraCodes.lean 27 declarations
IntervalEmbeddingFormulas.lean 3 declarations
IntervalHeightFormulas.lean 3 declarations
IntervalSequenceFormulas.lean 19 declarations
LeastSlotOwnerCodes.lean 21 declarations
LiftedCompressionFormulas.lean 10 declarations
LinkedMainInvariantCodes.lean 3 declarations
LinkedMainTransitionRawCodes.lean 12 declarations
LinkedProfileTransitionRawCodes.lean 5 declarations
MainLimitCoverageFormulas.lean 45 declarations
MainPrefixTraceStepFormulas.lean 10 declarations
MainPrefixValidityFormulas.lean 10 declarations
MainTransitionValidityCodes.lean 8 declarations
MapFamilyApplicationGraphs.lean 29 declarations
NameSupportFormulas.lean 5 declarations
NatUnionCodes.lean 39 declarations
NaturalSetCodes.lean 23 declarations
NaturalStepFormulas.lean 13 declarations
NonemptyTupleFields.lean 36 declarations
OrbitImageFormulas.lean 5 declarations
PairPushFilterFamilies.lean 11 declarations
ParentSupportCodes.lean 54 declarations
PartitionPrincipleFormula.lean 2 declarations
PreparedCertificateCodes.lean 8 declarations
PresentedGroupCodes.lean 63 declarations
PresentedRowAssignmentGraphs.lean 4 declarations
PreservedMainPrefixHistoryFormulas.lean 23 declarations
PrincipalSupportFormulas.lean 6 declarations
PrincipalTileRealization.lean 11 declarations
RationalCodeLaws.lean 15 declarations
RawCheckFormulas.lean 6 declarations
RawRenameFormulas.lean 10 declarations
RecursiveActionRealization.lean 18 declarations
RecursivePrimitiveFormulas.lean 7 declarations
RefinementDataHistoryEntryFormulas.lean 6 declarations
RefinementHistoryOrderOutputFormulas.lean 6 declarations
RefinementIndexActionFormulas.lean 3 declarations
RefinementValidityCodes.lean 6 declarations
RenamedEntryFormulas.lean 4 declarations
RepresentativeProductAgreement.lean 4 declarations
RootedSupportOwnerFunction.lean 10 declarations
RowAssignmentCutGraphLaws.lean 4 declarations
RowAssignmentTransitionFormulas.lean 7 declarations
SeparationEntryFormulas.lean 2 declarations
SeparationFulfillmentCodes.lean 18 declarations
SerializedChronologyFormulas.lean 11 declarations
SetPresentations.lean 13 declarations
SmallFunctionActionFormulas.lean 6 declarations
StrictLexHeightFormulas.lean 7 declarations
StructuralAssignmentActionFormulas.lean 4 declarations
StructuralRefinementHistoryFormulas.lean 3 declarations
SupportedCertificateFamilyFormulas.lean 5 declarations
SupportedCertificateRelations.lean 12 declarations
TaggedExtensionCodes.lean 13 declarations
TaggedGrowthLayerFormulas.lean 51 declarations
TaggedSumPresentations.lean 49 declarations
TaskCapFamilyCodes.lean 25 declarations
TaskRepresentativeCodes.lean 32 declarations
TaskTransportFormulas.lean 6 declarations
TileStarIncidenceRealization.lean 10 declarations
TupleRelationProducts.lean 6 declarations
UnionEntryFormula.lean 25 declarations
VisibilityProfileFormulas.lean 13 declarations