OAI/SetTheory/PartitionPrinciple/Definability/BatchGraphSetFormulas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.codedAttachmentOrder_mem line 13
2. def OAI.PartitionPilot.Forcing.SetFormula.sUnionSetFormula line 48
3. def OAI.PartitionPilot.Forcing.SetFormula.taggedExtensionSetFormula line 51
4. def OAI.PartitionPilot.Forcing.SetFormula.canonicalMeetSetFormula line 55
5. def OAI.PartitionPilot.Forcing.SetFormula.codedAttachmentOrderSetFormula line 58
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_exactBoundedSetFormula line 68
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_sUnionSetFormula line 77
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_taggedExtensionSetFormula line 91
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_canonicalMeetSetFormula line 103
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_codedAttachmentOrderSetFormula line 112
11. def OAI.PartitionPilot.Forcing.SetFormula.batchInsideSetFormula line 140
12. def OAI.PartitionPilot.Forcing.SetFormula.batchUpperSetFormula line 144
13. def OAI.PartitionPilot.Forcing.SetFormula.batchShadowSetFormula line 148
14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_exactReindexedBoundedSetFormula line 160
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_batchInsideSetFormula line 177
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_batchUpperSetFormula line 201
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_batchShadowSetFormula line 225