OAI/ModelTheory/Categoricity/ArrayMaps.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CHObstruction.Arrays.row_action_iff line 24
2. theorem OAI.CHObstruction.Arrays.col_action_iff line 38
3. theorem OAI.CHObstruction.Arrays.bit_relation_iff line 49
4. theorem OAI.CHObstruction.Arrays.group_add_iff line 62
5. theorem OAI.CHObstruction.Arrays.raw_map_index line 71
6. theorem OAI.CHObstruction.Arrays.raw_map_base line 79
7. theorem OAI.CHObstruction.Arrays.raw_map_group line 87
8. theorem OAI.CHObstruction.Arrays.raw_map_star line 95
9. theorem OAI.CHObstruction.Arrays.raw_map_row line 103
10. theorem OAI.CHObstruction.Arrays.raw_map_col line 111
11. theorem OAI.CHObstruction.Arrays.raw_map_label line 119
12. theorem OAI.CHObstruction.Arrays.raw_map_order line 127
13. theorem OAI.CHObstruction.Arrays.raw_map_incidence line 137
14. theorem OAI.CHObstruction.Arrays.raw_map_bit line 147
15. theorem OAI.CHObstruction.Arrays.raw_map_groupAdd line 159
16. theorem OAI.CHObstruction.Arrays.raw_map_starAdd line 171
17. theorem OAI.CHObstruction.Arrays.raw_map_rowAct line 183
18. theorem OAI.CHObstruction.Arrays.raw_map_colAct line 198
19. theorem OAI.CHObstruction.Arrays.tuple_list_eq_iff line 212
20. theorem OAI.CHObstruction.Arrays.base_point_eq_iff line 222
21. theorem OAI.CHObstruction.Arrays.raw_map_rowProjection line 227
22. theorem OAI.CHObstruction.Arrays.raw_map_colProjection line 235
23. theorem OAI.CHObstruction.Arrays.Map.rawRel line 246
24. theorem OAI.CHObstruction.Arrays.Map.rel line 266
25. def OAI.CHObstruction.Arrays.Map.id line 280
26. def OAI.CHObstruction.Arrays.Map.comp line 287
27. theorem OAI.CHObstruction.Arrays.Map.id_onPoint line 297
28. theorem OAI.CHObstruction.Arrays.Map.comp_onPoint line 301
29. theorem OAI.CHObstruction.Arrays.Map.ext_onPoint line 306
30. theorem OAI.CHObstruction.Arrays.Map.comp_id line 329
31. theorem OAI.CHObstruction.Arrays.Map.id_comp line 332