OAI/SetTheory/PartitionPrinciple/Definability/GroundSemanticStructuralFinalRefinements.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_antichains_below line 42
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_predense_prefix line 119
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_membershipAntichains_prefix line 231
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_finitePowerAntichains_prefix line 361
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_commonPowerAntichains line 482
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_commonEarlierPowerNames line 626
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_earlierPowerName line 749
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_commonRefinementNames line 873
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.semanticStructuralTrace_finalRefinementNames line 1036