OAI/SetTheory/PartitionPrinciple/Geometry/EligibleTaskCovariance.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.literalTask_fresh_iff line 12
2. theorem OAI.PartitionPilot.Forcing.literalTask_shadow_iff line 31
3. theorem OAI.PartitionPilot.Forcing.literalTask_upper_iff line 54
4. theorem OAI.PartitionPilot.Forcing.constantTask_inside_iff line 71
5. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.source_eq line 91
6. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.label_eq line 100
7. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.base_eq line 109
8. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.filter_eq line 119
9. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.fresh_iff line 129
10. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.shadow_covariant line 140
11. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.upper_covariant line 160
12. theorem OAI.PartitionPilot.Forcing.TaskTransportCode.inside_covariant line 176