OAI/Combinatorics/UniformKServer/RawRepresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.RawRepresentation.requests_injective line 15
2. theorem OAI.UniformKServer.RawRepresentation.config_injective line 18
3. theorem OAI.UniformKServer.RawRepresentation.lift_list line 25
4. theorem OAI.UniformKServer.RawRepresentation.lift_config line 30
5. abbrev OAI.UniformKServer.RawRepresentation.Index line 41
6. def OAI.UniformKServer.RawRepresentation.indexKey line 43
7. theorem OAI.UniformKServer.RawRepresentation.index_inj line 46
8. theorem OAI.UniformKServer.RawRepresentation.represents line 55