OAI/SetTheory/PartitionPrinciple/Definability/GroundPreparationEventSupportGraphs.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.BoundedFormula.eventSupportSetFormula line 12
2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_eventSupportSetFormula line 18
3. def OAI.PartitionPilot.Forcing.BoundedFormula.eventSupportGraphFormula line 38
4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_eventSupportGraphFormula line 41
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationEventUsedSupports_mem line 52
6. def OAI.PartitionPilot.Forcing.TransitiveGround.preparationEventSupportGraph line 68
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_preparationEventSupportGraph line 72
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationEventSupportGraph_function line 84
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationEventSupportGraph_mem line 97
10. def OAI.PartitionPilot.Forcing.TransitiveGround.preparationUsedSupportSequence line 115
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationUsedSupportSequence_ground_function line 118
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_preparationUsedSupportSequence line 134