OAI/SetTheory/PartitionPrinciple/Definability/GroundSemanticFairPreparationLimits.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.structuralForcingTrace_witnesses line 44
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_semanticStructuralForcingHistory line 59
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_semanticStructuralHistory line 102
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_binary_union_extension line 203
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_completeProjection line 277
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_exact_assignment_union line 354
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralFairPreparation_lower_bound line 454