OAI/Computability/DegreeRigidity/Constructibility/
473 declarations, 0 contain sorry, 0 declared as axioms; 101 files
Files
- CollectionHierarchyInternal.lean 5 declarations
- CollectionHierarchyRecursion.lean 1 declarations
- CollectionHierarchySyntax.lean 2 declarations
- ConstructibleBase.lean 6 declarations
- ConstructibleClosure.lean 7 declarations
- ConstructibleGroundReals.lean 8 declarations
- ConstructibleSatisfaction.lean 6 declarations
- ConstructibleSeparation.lean 6 declarations
- ConstructibleStages.lean 19 declarations
- ConstructibleSuccessorCode.lean 4 declarations
- ConstructibleTupleSpace.lean 12 declarations
- ConstructionDefinition.lean 4 declarations
- ConstructionHeightDomains.lean 1 declarations
- ConstructionInlining.lean 6 declarations
- ConstructionInputData.lean 13 declarations
- ConstructionStageBound.lean 4 declarations
- ContextDefinablePower.lean 7 declarations
- ContextHierarchyGraph.lean 4 declarations
- DecodedConstructionSyntax.lean 7 declarations
- DefSystemCertificate.lean 5 declarations
- DomainParameterizedSyntax.lean 6 declarations
- DomainSyntaxClosure.lean 4 declarations
- FiniteDefinitionTransfer.lean 2 declarations
- FiniteStageDefinition.lean 5 declarations
- FiniteStageSetBounds.lean 6 declarations
- FixedRelativeGround.lean 1 declarations
- HierarchyCertificatePower.lean 7 declarations
- HierarchyGraph.lean 9 declarations
- HierarchySyntax.lean 5 declarations
- HierarchyWitnessCollection.lean 4 declarations
- InternalConstructibleHierarchy.lean 6 declarations
- InternalHeightDomains.lean 5 declarations
- InternalHierarchyRecursion.lean 1 declarations
- InternalOmegaFixedPoint.lean 2 declarations
- InternalOmegaPower.lean 2 declarations
- InternalRankRecursion.lean 4 declarations
- OneRealConstructionDefinition.lean 1 declarations
- OneRealDefinitionSentence.lean 6 declarations
- ParameterFreeOrdinalStage.lean 1 declarations
- ParameterPersistentCollapse.lean 1 declarations
- PersistenceCriterion.lean 5 declarations
- PersistenceExtensionAbsoluteness.lean 5 declarations
- PersistenceRealClosure.lean 6 declarations
- PersistenceWitnessTree.lean 13 declarations
- PersistentConstruction.lean 3 declarations
- PersistentCountability.lean 6 declarations
- PersistentExtension.lean 2 declarations
- PersistentExtensionName.lean 2 declarations
- PersistentLocality.lean 6 declarations
- PersistentNonidentity.lean 6 declarations
- PersistentOneRealDefinition.lean 2 declarations
- PersistentPresentation.lean 4 declarations
- PersistentRestrictionCode.lean 1 declarations
- PersistentRestrictions.lean 25 declarations
- RelativeCohenJump.lean 5 declarations
- RelativeConstruction.lean 9 declarations
- RelativeDefCertificates.lean 2 declarations
- RelativeDegreeIdeal.lean 3 declarations
- RelativeHierarchyInternal.lean 2 declarations
- RelativeLevySchemas.lean 4 declarations
- RelativeModel.lean 16 declarations
- RelativeModelBounds.lean 4 declarations
- RelativeModelClosure.lean 10 declarations
- RelativeModelComparison.lean 3 declarations
- RelativeModelOrdinals.lean 5 declarations
- RelativeModelPower.lean 2 declarations
- RelativeModelSyntax.lean 6 declarations
- RelativeOmegaCertificates.lean 5 declarations
- RelativeOmegaLevels.lean 2 declarations
- RelativePersistentDescent.lean 2 declarations
- RelativePersistentExtension.lean 2 declarations
- RelativeSigmaReflection.lean 3 declarations
- RelativeSigmaSchemas.lean 5 declarations
- RelativeSigmaWitness.lean 4 declarations
- SeedBoundStageSyntax.lean 5 declarations
- SingleRealConstruction.lean 12 declarations
- UniformDefSuccessor.lean 3 declarations
- UniformDefinedSubsetName.lean 2 declarations
- UniformDefinitionSymmetry.lean 1 declarations
- UniformExtensionWitnessCover.lean 1 declarations
- UniformFragmentHull.lean 1 declarations
- UniformHeightDomains.lean 7 declarations
- UniformHierarchyStage.lean 5 declarations
- UniformInternalSatisfaction.lean 5 declarations
- UniformNameDescent.lean 3 declarations
- UniformNameValueCover.lean 1 declarations
- UniformOmegaLevels.lean 2 declarations
- UniformOrdinalDefinitionName.lean 1 declarations
- UniformOrdinalStageName.lean 2 declarations
- UniformOwnRealsName.lean 2 declarations
- UniformPowerName.lean 1 declarations
- UniformProductName.lean 1 declarations
- UniformSentenceSupport.lean 6 declarations
- UniformSeparationName.lean 1 declarations
- UniformSigmaDefinability.lean 9 declarations
- UniformSigmaHierarchy.lean 4 declarations
- UniformSigmaHull.lean 2 declarations
- UniformSigmaSeparationName.lean 1 declarations
- UniformSigmaUniqueName.lean 1 declarations
- UniformTruthRecursion.lean 6 declarations
- UniformTruthStep.lean 3 declarations