`OAI/Computability/DegreeRigidity/SetModels/`

1780 declarations, 0 contain sorry, 0 declared as axioms; 273 files

Files

BindCanonicalArithmetic.lean 4 declarations
ChoiceFromOrdinalCover.lean 7 declarations
ChoiceTrace.lean 9 declarations
ChoiceTraceExtension.lean 4 declarations
ChoiceTraceFormula.lean 9 declarations
ClosedPaddingCertificates.lean 1 declarations
CofinalPaddedDecoder.lean 2 declarations
CollapseCertificate.lean 6 declarations
CollapseCoding.lean 10 declarations
CollapseCollection.lean 2 declarations
CollapseCountWithoutChoice.lean 3 declarations
CollapseDenseWithoutChoice.lean 5 declarations
CollapseInternalCountingWithoutChoice.lean 2 declarations
CollapsePrefixAbsolute.lean 2 declarations
CollapseWithoutChoice.lean 3 declarations
ColumnSetFormula.lean 4 declarations
ConservativeExtension.lean 8 declarations
ContinuousCode.lean 12 declarations
CountableBound.lean 3 declarations
CountableElementaryHull.lean 15 declarations
CountableNameAvoidance.lean 3 declarations
CountableSetReal.lean 5 declarations
CountedOriginalRealQuotient.lean 1 declarations
CountedRealsPresentation.lean 3 declarations
CountedRegularBasis.lean 4 declarations
DecodingTheorem.lean 4 declarations
DegreeSetFormula.lean 3 declarations
DegreeUniverseWithoutChoice.lean 2 declarations
Degrees.lean 7 declarations
DenseInclusionExtension.lean 7 declarations
ElementaryAxioms.lean 7 declarations
ElementaryCheckedCode.lean 8 declarations
ElementaryCollapse.lean 11 declarations
ElementaryCollapsePoset.lean 12 declarations
ElementaryDefinableSets.lean 11 declarations
ElementaryDegreeHull.lean 9 declarations
ElementaryLanguage.lean 15 declarations
ElementaryModelIdeal.lean 6 declarations
ElementaryRealModel.lean 7 declarations
ElementarySatisfaction.lean 8 declarations
ElementarySchemas.lean 14 declarations
EnumerationConstruction.lean 6 declarations
EnumerationDecoding.lean 8 declarations
EnumerationTransport.lean 11 declarations
EvaluationNameCode.lean 2 declarations
ExactOmegaGraph.lean 2 declarations
ExtensionArithmeticRepresentative.lean 2 declarations
ExtensionBasicAxioms.lean 17 declarations
ExtensionChoice.lean 1 declarations
ExtensionPowerSet.lean 4 declarations
ExtensionSeparation.lean 1 declarations
ExtensionSigmaReplacement.lean 4 declarations
ExtensionSigmaSeparation.lean 1 declarations
ExtensionWitnessCover.lean 2 declarations
FiniteClosure.lean 6 declarations
FiniteOrdinalCode.lean 17 declarations
FinitePresentation.lean 1 declarations
FiniteSkolem.lean 6 declarations
FiniteSupport.lean 6 declarations
FixedArithmetic.lean 9 declarations
FixedArithmeticTailCone.lean 1 declarations
FragmentHull.lean 6 declarations
FullSetTruth.lean 4 declarations
GeneratedBooleanPart.lean 7 declarations
GeneratedHull.lean 7 declarations
IdealCopy.lean 1 declarations
IdealEnumeration.lean 1 declarations
IdealInterpretation.lean 31 declarations
IdealLift.lean 12 declarations
IdealLocality.lean 5 declarations
IdealPresentation.lean 3 declarations
IdealSelection.lean 8 declarations
InternalAtomicTruth.lean 4 declarations
InternalBooleanBits.lean 7 declarations
InternalBooleanDense.lean 8 declarations
InternalBooleanExtension.lean 6 declarations
InternalBooleanGeneric.lean 10 declarations
InternalBooleanGraph.lean 8 declarations
InternalBooleanIntermediate.lean 2 declarations
InternalBooleanName.lean 8 declarations
InternalBooleanProjection.lean 13 declarations
InternalBooleanSyntax.lean 9 declarations
InternalBooleanTop.lean 4 declarations
InternalBoundedTruth.lean 3 declarations
InternalCheckRecursion.lean 5 declarations
InternalCheckedValue.lean 2 declarations
InternalChoice.lean 6 declarations
InternalCollapseConditions.lean 16 declarations
InternalCollapseCounting.lean 8 declarations
InternalCollapseDense.lean 7 declarations
InternalCollapseExistence.lean 1 declarations
InternalColumnExtension.lean 4 declarations
InternalColumnProjection.lean 10 declarations
InternalCommonRequirements.lean 8 declarations
InternalContainer.lean 4 declarations
InternalCountableClosure.lean 11 declarations
InternalCountableEnumeration.lean 6 declarations
InternalCountableFamily.lean 2 declarations
InternalCountableFiniteUnion.lean 7 declarations
InternalCountableMap.lean 5 declarations
InternalCountableOrdinals.lean 10 declarations
InternalCountableProduct.lean 8 declarations
InternalCountableUnion.lean 1 declarations
InternalCoverInjection.lean 5 declarations
InternalDefinablePower.lean 2 declarations
InternalDenseFamily.lean 5 declarations
InternalDenseInclusion.lean 12 declarations
InternalFiniteEnumeration.lean 7 declarations
InternalFiniteExhaustion.lean 10 declarations
InternalFiniteSubsets.lean 7 declarations
InternalFixedPoint.lean 1 declarations
InternalFunctionOrbit.lean 7 declarations
InternalGeneratedAlgebra.lean 8 declarations
InternalGenericFilter.lean 3 declarations
InternalGenericSequence.lean 6 declarations
InternalGraphEquiv.lean 5 declarations
InternalHartogs.lean 1 declarations
InternalHomogeneousTruth.lean 2 declarations
InternalHull.lean 14 declarations
InternalInfinity.lean 21 declarations
InternalInverseGraph.lean 6 declarations
InternalInverseIso.lean 1 declarations
InternalMinimalSelector.lean 11 declarations
InternalNameEvaluation.lean 8 declarations
InternalNameValidity.lean 2 declarations
InternalNaturalCheckSequence.lean 1 declarations
InternalNaturalRelationReal.lean 6 declarations
InternalNiceName.lean 4 declarations
InternalOrderIsoTransport.lean 8 declarations
InternalOrdinalCodes.lean 5 declarations
InternalOrdinalEnumeration.lean 1 declarations
InternalOrdinalSubset.lean 9 declarations
InternalPositiveNameFamily.lean 3 declarations
InternalPresentationEnumeration.lean 2 declarations
InternalPrimitiveGraph.lean 2 declarations
InternalProductBijection.lean 6 declarations
InternalProjectedGeneric.lean 8 declarations
InternalQuotientConditions.lean 9 declarations
InternalQuotientCountability.lean 2 declarations
InternalQuotientExtension.lean 3 declarations
InternalQuotientGeneric.lean 3 declarations
InternalQuotientLifting.lean 2 declarations
InternalQuotientRequirement.lean 4 declarations
InternalRealQuotient.lean 7 declarations
InternalRegularAlgebra.lean 16 declarations
InternalRegularOperations.lean 18 declarations
InternalRegularOrder.lean 12 declarations
InternalRegularSplitter.lean 2 declarations
InternalRegularTree.lean 2 declarations
InternalRelationCollapse.lean 7 declarations
InternalRelationSelection.lean 6 declarations
InternalSameNameGeneric.lean 3 declarations
InternalSatisfactionSlice.lean 7 declarations
InternalSequenceRange.lean 6 declarations
InternalSerialSelection.lean 4 declarations
InternalShuffleGeneric.lean 2 declarations
InternalShuffleSets.lean 14 declarations
InternalSigmaSequence.lean 2 declarations
InternalSingletonColumn.lean 7 declarations
InternalStructureCollapse.lean 9 declarations
InternalSubsetSequence.lean 1 declarations
InternalUncountableComplement.lean 4 declarations
InternalUncountableSentence.lean 8 declarations
InternalUniformization.lean 5 declarations
IntersectionName.lean 3 declarations
ModelArithmeticComprehension.lean 4 declarations
ModelArithmeticTreeDescent.lean 7 declarations
ModelAutomorphismInterpretation.lean 5 declarations
ModelDegreeCodes.lean 6 declarations
ModelDegreeOrder.lean 12 declarations
ModelDegreeUniverse.lean 6 declarations
ModelIdealInterpretation.lean 5 declarations
ModelIterationFormula.lean 4 declarations
ModelIterationTrace.lean 6 declarations
ModelNaturalNumbers.lean 7 declarations
ModelOmegaJump.lean 4 declarations
ModelOrderSatisfaction.lean 13 declarations
ModelPersistenceReals.lean 3 declarations
ModelPersistenceSatisfaction.lean 6 declarations
ModelPersistentGraph.lean 3 declarations
ModelPresentationSets.lean 6 declarations
ModelProducts.lean 5 declarations
ModelRealOperations.lean 5 declarations
ModelReals.lean 10 declarations
MostowskiCollapse.lean 9 declarations
NameDifferenceDense.lean 3 declarations
NameEncoding.lean 7 declarations
NameEvaluationGraph.lean 2 declarations
NameExtension.lean 15 declarations
NameSupport.lean 5 declarations
NameUnionCode.lean 15 declarations
NameValidity.lean 12 declarations
NameValueCover.lean 6 declarations
NoNewOrdinals.lean 3 declarations
OrderedNameCode.lean 11 declarations
ParametricEval.lean 1 declarations
PresentationEnumeration.lean 9 declarations
PresentationGraphSet.lean 5 declarations
PresentedDegreeEmbedding.lean 6 declarations
ProjectedArithmeticOutputCone.lean 1 declarations
ProjectedArithmeticOutputName.lean 2 declarations
RecursiveNameSymmetry.lean 13 declarations
RecursiveNames.lean 11 declarations
RecursiveOmegaBound.lean 3 declarations
RecursiveSumBound.lean 1 declarations
RegularBinaryTree.lean 15 declarations
RegularCodeSplitting.lean 10 declarations
RegularCompletion.lean 14 declarations
RegularDecisionPartition.lean 11 declarations
RegularProjection.lean 5 declarations
RegularTreeCofinality.lean 5 declarations
RegularTreeCompatibility.lean 3 declarations
RegularTreeExtension.lean 2 declarations
RegularTreeFilter.lean 6 declarations
RegularTreeRecovery.lean 7 declarations
RegularTreeRun.lean 8 declarations
RelationCoding.lean 5 declarations
RelationCollapse.lean 12 declarations
RelationHull.lean 20 declarations
RelationPresentation.lean 22 declarations
RestrictedName.lean 7 declarations
RestrictedOmegaRecursion.lean 2 declarations
SelectedColumnArithmeticCone.lean 1 declarations
SelectedColumnPrefixProgram.lean 1 declarations
SetDegreeDecoding.lean 11 declarations
SetModelActionDecoding.lean 3 declarations
SetModelActionSatisfaction.lean 7 declarations
SetModelAddition.lean 11 declarations
SetModelArithmeticClosure.lean 5 declarations
SetModelArithmeticDischarge.lean 3 declarations
SetModelArithmeticInterface.lean 3 declarations
SetModelArithmeticSyntax.lean 14 declarations
SetModelArithmeticTree.lean 5 declarations
SetModelColumns.lean 7 declarations
SetModelCountability.lean 11 declarations
SetModelCountableExtensions.lean 1 declarations
SetModelCountablePresentation.lean 2 declarations
SetModelDegreeUniverse.lean 3 declarations
SetModelFunctionGraphs.lean 12 declarations
SetModelFunctionIteration.lean 8 declarations
SetModelFunctionPairing.lean 6 declarations
SetModelGraphImage.lean 5 declarations
SetModelGraphPresentation.lean 4 declarations
SetModelIdealDecoding.lean 2 declarations
SetModelIdealSatisfaction.lean 5 declarations
SetModelInternalRelations.lean 6 declarations
SetModelIteration.lean 12 declarations
SetModelJoin.lean 5 declarations
SetModelMultiplication.lean 6 declarations
SetModelMultiplicationStep.lean 15 declarations
SetModelOmegaJump.lean 2 declarations
SetModelPairing.lean 10 declarations
SetModelPersistence.lean 3 declarations
SetModelPersistenceDecoding.lean 1 declarations
SetModelPersistentSatisfaction.lean 8 declarations
SetModelPresentedCountability.lean 7 declarations
SetModelPrimrec.lean 8 declarations
SetModelReals.lean 12 declarations
SetModelRecursion.lean 5 declarations
SetModelSequences.lean 10 declarations
SetModelTreeRelations.lean 9 declarations
SetPresentationDecoding.lean 13 declarations
ShuffleRequirements.lean 24 declarations
SkolemHull.lean 9 declarations
SkolemOperations.lean 8 declarations
SmallWitnessBound.lean 3 declarations
TransitiveNameModel.lean 16 declarations
TwoRealHull.lean 3 declarations
UnionIteration.lean 14 declarations
ValidFirstUncountable.lean 5 declarations
WeakNameAvoidance.lean 2 declarations
WeakNameDifference.lean 2 declarations
WeakRealDescent.lean 1 declarations