OAI/SetTheory/PartitionPrinciple/Geometry/GroundLiteralTaskFieldRecognition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.literalTaskBound_mem line 12
2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.literalTaskFieldBound_mem line 24
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.literalTaskFieldGraph_mem line 31
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.literalTaskFieldFamilies line 55
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.constantFamilyGraph_mem line 67
6. def OAI.PartitionPilot.Forcing.SetFormula.literalTaskFieldSetFormula line 85
7. def OAI.PartitionPilot.Forcing.SetFormula.constantFamilySetFormula line 89
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_literalTaskFieldSetFormula line 102
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_constantFamilySetFormula line 114
10. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_literalTaskField line 134
11. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_constantFamily line 142