OAI/SetTheory/PartitionPrinciple/Forcing/
2584 declarations, 0 contain sorry, 0 declared as axioms; 220 files
Files
- ActionPostcompositionCodes.lean 24 declarations
- ActiveNameImageSymmetry.lean 12 declarations
- AllSupportFamilies.lean 5 declarations
- AtomicTruth.lean 7 declarations
- ChronologicalTransport.lean 3 declarations
- CodedDenseOrders.lean 6 declarations
- CodedRecursiveTaskActions.lean 35 declarations
- CompleteProjectionFilterLifts.lean 1 declarations
- ConditionQuantifiers.lean 17 declarations
- CrossStageMembershipNameActions.lean 4 declarations
- DenseInterpolation.lean 23 declarations
- EligibleBatchEquivariance.lean 8 declarations
- EvaluatedDomains.lean 56 declarations
- ExternalAction.lean 12 declarations
- ExternalFilterBases.lean 11 declarations
- ExternalWordInverseEvaluation.lean 2 declarations
- FinalFilterLocalization.lean 6 declarations
- FinitePrincipalNameSupports.lean 46 declarations
- FixedTop.lean 22 declarations
- FixedTopProfilePreservation.lean 3 declarations
- FlatConditionSystems.lean 3 declarations
- FlatLimitConditionCodes.lean 7 declarations
- FlatSuccessorConditionUnions.lean 5 declarations
- FlatSuccessorConditions.lean 7 declarations
- ForcingHistoryTestDecomposition.lean 15 declarations
- GeneratedMeetFilters.lean 8 declarations
- GenericPartialFunctions.lean 65 declarations
- GreedyAntichainTraces.lean 12 declarations
- GroundAbsentLiftClassTransport.lean 1 declarations
- GroundActionFilterImages.lean 3 declarations
- GroundActionPostcomposition.lean 6 declarations
- GroundBatchEarlierLayerWitnesses.lean 22 declarations
- GroundBinaryRowNameCodes.lean 9 declarations
- GroundBinaryRowNameSupportBounds.lean 1 declarations
- GroundBinaryRowNames.lean 5 declarations
- GroundBinaryRowStructuralDataBoundActions.lean 1 declarations
- GroundChronologicalTransitionTransport.lean 5 declarations
- GroundChronologyWitnessSelection.lean 3 declarations
- GroundCompleteProjectionAtomicTruth.lean 5 declarations
- GroundCompleteProjectionGenericity.lean 17 declarations
- GroundCompressionIncomingWitnessRanks.lean 9 declarations
- GroundCompressionSerializationTransport.lean 1 declarations
- GroundCountableFunctionForcing.lean 5 declarations
- GroundDefinableRefinementNameGraphs.lean 18 declarations
- GroundEligibleActionStep.lean 3 declarations
- GroundEligibleBatchActionRecognition.lean 7 declarations
- GroundExternalLayerWitnessRanks.lean 7 declarations
- GroundExternalOldAction.lean 6 declarations
- GroundExternalStarSupports.lean 6 declarations
- GroundFairPreparationConditionSequences.lean 5 declarations
- GroundFilterCopies.lean 3 declarations
- GroundFilterPullbackRecovery.lean 1 declarations
- GroundFixedIndexAssignmentSlices.lean 7 declarations
- GroundFixedPoints.lean 6 declarations
- GroundFixedTopStep.lean 17 declarations
- GroundFixedTopTerminal.lean 3 declarations
- GroundFlatLimitConditions.lean 5 declarations
- GroundFlatSuccessorFullActionGraph.lean 20 declarations
- GroundFlatSuccessorNameGraphs.lean 10 declarations
- GroundForcingHistoryLimitConnection.lean 3 declarations
- GroundForcingHistoryOrders.lean 5 declarations
- GroundForcingHistorySuccessors.lean 21 declarations
- GroundGraphValueDescendantWitnesses.lean 25 declarations
- GroundIdealProjections.lean 5 declarations
- GroundInaccessibleConditions.lean 9 declarations
- GroundIndexedGraphNameFamilies.lean 17 declarations
- GroundInvariantNamePowers.lean 3 declarations
- GroundLayerWitnessPushforward.lean 1 declarations
- GroundMainConditionalTotality.lean 7 declarations
- GroundMainFinalCompressedNameForcing.lean 1 declarations
- GroundMainFinalRectangleActionData.lean 1 declarations
- GroundMainFinalRowNiceNames.lean 1 declarations
- GroundMainFinalRowSupport.lean 9 declarations
- GroundMainFinalSameFilterPreparationBatch.lean 1 declarations
- GroundMainFinalStageOneForcing.lean 1 declarations
- GroundMainFinalStageOneGroundAction.lean 3 declarations
- GroundMainFinalStageThreeAction.lean 3 declarations
- GroundMainFinalStageThreeNameLifting.lean 11 declarations
- GroundMainFinalStageTwoAction.lean 1 declarations
- GroundMainFinalStageTwoConditions.lean 1 declarations
- GroundMainFinalStageTwoNameLifting.lean 3 declarations
- GroundMainFinalStructuralCommonSupportInduction.lean 22 declarations
- GroundMainFinalStructuralDecidingAntichains.lean 2 declarations
- GroundMainFinalStructuralPositionSupport.lean 2 declarations
- GroundMainFinalStructuralRefinementNames.lean 3 declarations
- GroundMainFinalStructuralSupportPreparation.lean 3 declarations
- GroundMainFinalSupportConstruction.lean 3 declarations
- GroundMainFinalSupportedCertificateFamilies.lean 13 declarations
- GroundMainFinalSymmetricRefinementOutputs.lean 1 declarations
- GroundMainPrefixInsertionFamilyTransport.lean 8 declarations
- GroundMainPrefixLimitActionLaws.lean 18 declarations
- GroundMainPrefixLimitLayerWitnesses.lean 6 declarations
- GroundMainPrefixPriorLayerWitnesses.lean 1 declarations
- GroundMainPrefixRectangleBoundTransport.lean 1 declarations
- GroundMixtureNames.lean 18 declarations
- GroundNameSequenceForcingWitness.lean 16 declarations
- GroundNameSequenceValues.lean 29 declarations
- GroundNiceNameGraphs.lean 6 declarations
- GroundNiceNameNormalization.lean 25 declarations
- GroundNicePreparationWitnessBounds.lean 9 declarations
- GroundNiceRefinementClassSupports.lean 1 declarations
- GroundNiceRefinementIndexActionLaws.lean 24 declarations
- GroundNiceSupportEvaluation.lean 6 declarations
- GroundOrdinaryEqualityDecisionFusion.lean 7 declarations
- GroundOrdinaryMembershipAntichainFamilies.lean 16 declarations
- GroundOutsideRowNames.lean 46 declarations
- GroundPairNameFamilies.lean 7 declarations
- GroundPreparationForcing.lean 10 declarations
- GroundPreparedCertificateActionPackages.lean 16 declarations
- GroundPreparedWitnessSelections.lean 6 declarations
- GroundPrincipalSupportZF.lean 8 declarations
- GroundProductActions.lean 56 declarations
- GroundProductSizeWitnesses.lean 2 declarations
- GroundProjectedRowChooserWitnesses.lean 11 declarations
- GroundPushFilters.lean 5 declarations
- GroundRankedCompressionFieldsTransport.lean 8 declarations
- GroundRankedFixedTopSerialization.lean 5 declarations
- GroundRawNiceNameGraphs.lean 9 declarations
- GroundRawPreparedFamilyConditionPersistence.lean 3 declarations
- GroundRawRefinementStageWitnesses.lean 37 declarations
- GroundRawRowAssignmentActions.lean 16 declarations
- GroundRawStageRefinementTestActions.lean 17 declarations
- GroundRecordedPreparationSupportInclusions.lean 5 declarations
- GroundRecursiveActions.lean 53 declarations
- GroundRecursiveRowNameActions.lean 15 declarations
- GroundRefinementAssignmentActionFamilies.lean 39 declarations
- GroundRefinementAssignmentLabelNames.lean 1 declarations
- GroundRefinementCollisionSymmetry.lean 2 declarations
- GroundRefinementDiagonalConditions.lean 1 declarations
- GroundRefinementValidityForcing.lean 3 declarations
- GroundRenamedNameFamilyBounds.lean 21 declarations
- GroundRepresentativeAntichainBounds.lean 2 declarations
- GroundRepresentedDomainConditions.lean 24 declarations
- GroundRestrictedActions.lean 2 declarations
- GroundRowAssignmentActions.lean 6 declarations
- GroundRowGenerics.lean 15 declarations
- GroundRowTermSetNames.lean 7 declarations
- GroundRowTupleEvaluation.lean 3 declarations
- GroundSelectedOrbitNameFamilies.lean 7 declarations
- GroundSeparatedRowConditions.lean 3 declarations
- GroundSharedConditionalNames.lean 18 declarations
- GroundSizeWitnesses.lean 7 declarations
- GroundSmallFunctionPermutations.lean 35 declarations
- GroundStageOneDataBoundFixation.lean 6 declarations
- GroundStageOneDataBoundSmallFixation.lean 4 declarations
- GroundStageOneFlatConditions.lean 9 declarations
- GroundStageOneGenericProjection.lean 2 declarations
- GroundStageOneGroundAction.lean 26 declarations
- GroundStageOneNameLiftFamilies.lean 16 declarations
- GroundStageOneNameLifting.lean 53 declarations
- GroundStageOneRawNames.lean 5 declarations
- GroundStageThreeActionInputs.lean 24 declarations
- GroundStageThreeDataBoundFixation.lean 11 declarations
- GroundStageTwoActionInputs.lean 22 declarations
- GroundStageTwoConditionTop.lean 36 declarations
- GroundStageTwoNameGraphs.lean 10 declarations
- GroundStageTwoNameLiftFamilies.lean 4 declarations
- GroundStageTwoNamePositionSupports.lean 10 declarations
- GroundStoredPreparedFamilyActions.lean 27 declarations
- GroundStoredStructuralRequestActions.lean 8 declarations
- GroundStructuralForcingActionGraphs.lean 8 declarations
- GroundStructuralForcingHistoryConstruction.lean 21 declarations
- GroundSupportedCertificateFamilyDecisions.lean 6 declarations
- GroundSupportedCertificateProfiles.lean 2 declarations
- GroundSymmetricCollection.lean 2 declarations
- GroundSymmetricPowerSet.lean 6 declarations
- GroundTaskBearingSuccessorWitness.lean 1 declarations
- GroundTestedMeetFilters.lean 17 declarations
- GroundUnionSizeWitnesses.lean 17 declarations
- GroundVaryingFamilyEvaluation.lean 12 declarations
- GrowthLayerWitnessRestrictions.lean 7 declarations
- IdealChain.lean 31 declarations
- IdealInsertionProfileTransport.lean 2 declarations
- IndexedTupleNames.lean 60 declarations
- InitialAction.lean 20 declarations
- InitialRecursiveActionAgreement.lean 4 declarations
- InitialRowForcing.lean 63 declarations
- LimitAction.lean 14 declarations
- MainPrefixConditionalStepCodes.lean 5 declarations
- MainPrefixConditionalTraceLaws.lean 2 declarations
- MeetOrderPosetActions.lean 6 declarations
- NameFamilySetTransport.lean 3 declarations
- NameMixingRanks.lean 45 declarations
- NameOrbitBounds.lean 24 declarations
- NamePresentationEquivalences.lean 9 declarations
- NameRenameSteps.lean 22 declarations
- NatActionUnions.lean 2 declarations
- OrbitPairGraphNames.lean 63 declarations
- OwnerBirthLayerTransport.lean 5 declarations
- PairFamilyEvaluation.lean 10 declarations
- PreparedWitnessCertificateGraphs.lean 4 declarations
- PresentedMeetActionCodes.lean 4 declarations
- ProfileTransport.lean 7 declarations
- RecursiveAction.lean 31 declarations
- RecursiveNextTaskActions.lean 4 declarations
- RecursiveRefinementUnionConditions.lean 2 declarations
- RefinementAssignmentActionLaws.lean 4 declarations
- RefinementAssignmentLabelActions.lean 3 declarations
- RefinementAssignmentLabelNames.lean 15 declarations
- RefinementCoarseImageNames.lean 10 declarations
- RefinementDataBoundActions.lean 2 declarations
- RelationActionFamilies.lean 5 declarations
- RenamedPairNameFamilies.lean 29 declarations
- RequestedSupportOwners.lean 6 declarations
- RootedSupportOwners.lean 9 declarations
- RowNames.lean 13 declarations
- RowSupportDescent.lean 3 declarations
- SmallCodedMeetActions.lean 13 declarations
- StageOneEvaluatedAssignments.lean 6 declarations
- StageThreeAssignmentTestActions.lean 6 declarations
- StageTwoAssignmentTestActions.lean 8 declarations
- StageTwoConditionUnions.lean 5 declarations
- StructuralAssignmentActionGraphs.lean 5 declarations
- StructuralAssignmentActionLaws.lean 1 declarations
- StructuralForcingStageWitnessStep.lean 21 declarations
- SymmetricGroundForcing.lean 16 declarations
- TaskTransportCodes.lean 11 declarations
- UniformGroundNames.lean 24 declarations
- UniformGroundSizeWitnesses.lean 6 declarations
- UniqueFiberForcing.lean 4 declarations