OAI/Computability/DegreeRigidity/CohenForcing/
670 declarations, 0 contain sorry, 0 declared as axioms; 108 files
Files
- AtomicForcing.lean 10 declarations
- BoundedForcing.lean 10 declarations
- BoundedForcingCode.lean 2 declarations
- CheckedForcingRelation.lean 3 declarations
- CohenAbsorptionGeneric.lean 1 declarations
- CohenAbsorptionTree.lean 2 declarations
- CohenAntichainFamilySupport.lean 3 declarations
- CohenAntichainSelector.lean 8 declarations
- CohenAntichainSequence.lean 7 declarations
- CohenAntichainStages.lean 12 declarations
- CohenBorelForcing.lean 15 declarations
- CohenChainCondition.lean 4 declarations
- CohenColumnAbsorption.lean 1 declarations
- CohenColumnPrefixCone.lean 2 declarations
- CohenColumnPrefixGeneric.lean 2 declarations
- CohenColumnRealName.lean 9 declarations
- CohenColumnRealValue.lean 7 declarations
- CohenColumns.lean 15 declarations
- CohenCompleteness.lean 3 declarations
- CohenConditionCode.lean 9 declarations
- CohenConservative.lean 5 declarations
- CohenCoordinates.lean 12 declarations
- CohenCountedAntichain.lean 3 declarations
- CohenDisjointPrefixPair.lean 1 declarations
- CohenEffectiveGeneric.lean 10 declarations
- CohenFactorIteration.lean 2 declarations
- CohenFactorReconstruction.lean 4 declarations
- CohenFactorRequirement.lean 3 declarations
- CohenFilterReal.lean 6 declarations
- CohenFiniteAntichains.lean 1 declarations
- CohenFiniteFlip.lean 5 declarations
- CohenFreshColumn.lean 3 declarations
- CohenGenericUnion.lean 7 declarations
- CohenGroundGeneric.lean 7 declarations
- CohenGroundJump.lean 3 declarations
- CohenGroundPoset.lean 14 declarations
- CohenGroundProgram.lean 3 declarations
- CohenHalting.lean 19 declarations
- CohenInternalAntichain.lean 2 declarations
- CohenInternalDecision.lean 7 declarations
- CohenInternalSupport.lean 9 declarations
- CohenIteratedAbsorption.lean 1 declarations
- CohenLiteralAbsorption.lean 2 declarations
- CohenLowness.lean 10 declarations
- CohenManyAbsorption.lean 1 declarations
- CohenNiceNameConstruction.lean 5 declarations
- CohenNiceNames.lean 10 declarations
- CohenPartitionBridge.lean 4 declarations
- CohenPartitionJoint.lean 1 declarations
- CohenPartitionRealization.lean 2 declarations
- CohenPrefixDensity.lean 5 declarations
- CohenPrefixHull.lean 2 declarations
- CohenPrefixOverwrite.lean 3 declarations
- CohenPrefixReconstruction.lean 6 declarations
- CohenProductFilters.lean 12 declarations
- CohenProductSplitting.lean 8 declarations
- CohenProgramTotality.lean 2 declarations
- CohenProjectedNameLift.lean 1 declarations
- CohenRecursiveName.lean 9 declarations
- CohenRemainderTransport.lean 1 declarations
- CohenRun.lean 4 declarations
- CohenSizeLevels.lean 8 declarations
- CohenSymmetry.lean 19 declarations
- CohenUntouchedGeneric.lean 2 declarations
- CohenUnusedTransport.lean 1 declarations
- CohenWordCodeGraph.lean 11 declarations
- CountableForcing.lean 16 declarations
- CountedCohenConditions.lean 5 declarations
- EffectiveForcing.lean 3 declarations
- EncodedForcing.lean 18 declarations
- ForcingProjection.lean 16 declarations
- ForcingRequirements.lean 5 declarations
- ForcingSymmetry.lean 10 declarations
- ForcingWitnessCollection.lean 4 declarations
- FullSetForcing.lean 4 declarations
- InternalCohenBitFlip.lean 10 declarations
- InternalCohenBooleanReading.lean 1 declarations
- InternalCohenColumnReading.lean 1 declarations
- InternalCohenConditions.lean 18 declarations
- InternalCohenFactor.lean 10 declarations
- InternalCohenFilters.lean 12 declarations
- InternalCohenHomogeneity.lean 7 declarations
- InternalCohenName.lean 8 declarations
- InternalCohenOddHits.lean 5 declarations
- InternalCohenPartition.lean 8 declarations
- InternalCohenProjectedGeneric.lean 8 declarations
- InternalCohenProjectionSymmetry.lean 4 declarations
- InternalCohenReindex.lean 10 declarations
- InternalCohenRequirements.lean 4 declarations
- InternalCohenRestriction.lean 13 declarations
- InternalCohenSupportedValue.lean 4 declarations
- InternalCohenTailHomogeneity.lean 7 declarations
- InternalCohenTailTruth.lean 2 declarations
- InternalCohenUnusedColumns.lean 2 declarations
- InternalCohenValue.lean 5 declarations
- QuotientDense.lean 8 declarations
- QuotientNames.lean 6 declarations
- RestrictedForcingFilter.lean 6 declarations
- SigmaForcing.lean 3 declarations
- SparseCohenFilter.lean 4 declarations
- SparseCohenPrefixGeneric.lean 3 declarations
- SparseCohenRealName.lean 7 declarations
- SparseCohenRealValue.lean 2 declarations
- TaggedProductConditions.lean 13 declarations
- TaggedProductExtension.lean 1 declarations
- TaggedProductGeneric.lean 9 declarations
- TaggedProductRecovery.lean 6 declarations
- WeakForcingCode.lean 1 declarations