OAI/SetTheory/PartitionPrinciple/Definability/GroundVaryingPreparationRelations.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.TransitiveGround.StoredPreparationCode line 13
2. def OAI.PartitionPilot.Forcing.TransitiveGround.transitionShape line 22
3. def OAI.PartitionPilot.Forcing.TransitiveGround.transitionBody line 35
4. def OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationFormula line 46
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_storedPreparationFormula line 50
6. def OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationRelation line 117
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_storedPreparationRelation line 127
8. def OAI.PartitionPilot.Forcing.TransitiveGround.preparationEntryFormula line 147
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preparationEntryFormula line 156
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationRelation_mem line 195
11. def OAI.PartitionPilot.Forcing.TransitiveGround.VaryingPreparationCode line 242
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.varyingPreparationCode_pair_iff line 251
13. def OAI.PartitionPilot.Forcing.TransitiveGround.varyingShape line 268
14. def OAI.PartitionPilot.Forcing.TransitiveGround.varyingBody line 282
15. def OAI.PartitionPilot.Forcing.TransitiveGround.varyingPreparationFormula line 293
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_varyingPreparationFormula line 297
17. def OAI.PartitionPilot.Forcing.TransitiveGround.varyingPreparationRelation line 380
18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_varyingPreparationRelation line 389
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.varyingPreparationRelation_mem line 407