OAI/ModelTheory/Categoricity/Colors.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CHObstruction.Colors.Sequence line 15
  2. def OAI.CHObstruction.Colors.equivalent line 17
  3. def OAI.CHObstruction.Colors.eventualSetoid line 19
  4. abbrev OAI.CHObstruction.Colors.Color line 31
  5. def OAI.CHObstruction.Colors.color line 33
  6. theorem OAI.CHObstruction.Colors.color_eq_iff line 35
  7. def OAI.CHObstruction.Colors.repeatSequence line 38
  8. theorem OAI.CHObstruction.Colors.repeat_injective line 40
  9. theorem OAI.CHObstruction.Colors.cardinal line 54
  10. abbrev OAI.CHObstruction.Colors.Palette line 60
  11. theorem OAI.CHObstruction.Colors.palette_cardinal line 62
  12. def OAI.CHObstruction.Colors.representative line 65
  13. theorem OAI.CHObstruction.Colors.representative_color line 67
  14. theorem OAI.CHObstruction.Colors.function_bound line 69
  15. theorem OAI.CHObstruction.Colors.diagram_bound line 81
  16. def OAI.CHObstruction.Colors.code line 103
  17. abbrev OAI.CHObstruction.Tuples.Tuple line 119
  18. def OAI.CHObstruction.Tuples.sub line 121
  19. theorem OAI.CHObstruction.Tuples.sub_refl line 124
  20. theorem OAI.CHObstruction.Tuples.sub_comp line 129
  21. theorem OAI.CHObstruction.Tests.embedding_refl line 137
  22. def OAI.CHObstruction.Tests.Passes line 146
  23. def OAI.CHObstruction.Tests.Test line 152
  24. instance OAI.CHObstruction.Tests.emptyLabel line 155
  25. def OAI.CHObstruction.Tests.emptyDiagram line 159
  26. theorem OAI.CHObstruction.Tests.empty_valid line 164
  27. theorem OAI.CHObstruction.Tests.empty_unique line 169
  28. theorem OAI.CHObstruction.Tests.no_pattern line 173