OAI/Computability/Superstring/UpperController.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Superstring.CollectionCode.complete line 8
2. theorem OAI.Superstring.CollectionCode.Model.first_eq line 26
3. theorem OAI.Superstring.CollectionCode.Model.last_eq line 29
4. theorem OAI.Superstring.CollectionCode.Model.complete_spec line 33
5. structure OAI.Superstring.CollectionCode.RequestAt line 147
6. def OAI.Superstring.CollectionCode.RequestAt.hosted line 165
7. def OAI.Superstring.CollectionCode.RequestAt.request line 184
8. theorem OAI.Superstring.CollectionCode.RequestAt.data_rep line 202
9. theorem OAI.Superstring.CollectionCode.RequestAt.entry_eq line 208
10. theorem OAI.Superstring.CollectionCode.Model.requestAt line 216
11. def OAI.Superstring.CollectionCode.entries line 230
12. def OAI.Superstring.CollectionCode.requestedData line 232
13. def OAI.Superstring.CollectionCode.fibrePool line 234
14. def OAI.Superstring.CollectionCode.SourcesDistinct line 238
15. theorem OAI.Superstring.CollectionCode.Model.fibrePool_complete line 242