OAI/SetTheory/PartitionPrinciple/Geometry/GroundTaskRepresentativeRecognition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.groundRelationsFormula line 11
2. def OAI.PartitionPilot.Forcing.SetFormula.groundMeetFiltersFormula line 14
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundRelationsFormula line 22
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundMeetFiltersFormula line 33
5. def OAI.PartitionPilot.Forcing.SetFormula.groundLiteralTaskFieldFormula line 49
6. def OAI.PartitionPilot.Forcing.SetFormula.taskTransportSetFormula line 54
7. def OAI.PartitionPilot.Forcing.SetFormula.groundTaskTransportFormula line 58
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundLiteralTaskFieldFormula line 74
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_taskTransportSetFormula line 104
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundTaskTransportFormula line 121
11. def OAI.PartitionPilot.Forcing.TaskRepresentativesCode line 168
12. def OAI.PartitionPilot.Forcing.BoundedFormula.taskRepresentativesFormula line 174
13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_taskRepresentativesFormula line 180
14. def OAI.PartitionPilot.Forcing.SetFormula.groundTaskRepresentativesFormula line 202
15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groundTaskRepresentativesFormula line 217