OAI/ModelTheory/Categoricity/ArrayEmbeddings.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CHObstruction.Tests.congr line 17
  2. theorem OAI.CHObstruction.Tests.map line 24
  3. def OAI.CHObstruction.Arrays.Map.colors line 40
  4. theorem OAI.CHObstruction.Arrays.color_column line 43
  5. theorem OAI.CHObstruction.Arrays.Map.colors_base line 52
  6. def OAI.CHObstruction.Arrays.Map.exceptions line 65
  7. theorem OAI.CHObstruction.Arrays.Map.exceptions_countable line 69
  8. theorem OAI.CHObstruction.Arrays.Map.test_away line 78
  9. structure OAI.CHObstruction.Arrays.Map.Strong line 91
  10. theorem OAI.CHObstruction.Arrays.Map.id_strong line 96
  11. theorem OAI.CHObstruction.Arrays.Map.comp_colors_base line 103
  12. theorem OAI.CHObstruction.Arrays.Map.comp_colors_outside line 122
  13. theorem OAI.CHObstruction.Arrays.Map.Strong.comp line 136
  14. def OAI.CHObstruction.Tuples.mapEquiv line 166
  15. theorem OAI.CHObstruction.Arrays.Map.surjective line 187
  16. def OAI.CHObstruction.Arrays.Map.equiv line 216
  17. def OAI.CHObstruction.Arrays.countableMap line 220
  18. theorem OAI.CHObstruction.Arrays.countable_isomorphic line 233
  19. theorem OAI.CHObstruction.Arrays.Map.strong_of_surjective line 239
  20. theorem OAI.CHObstruction.Arrays.Map.object_of_surjective line 247
  21. def OAI.CHObstruction.Tuples.entriesList line 270
  22. theorem OAI.CHObstruction.Tuples.entriesList_injective line 272
  23. structure OAI.CHObstruction.Arrays.RawEmbedding line 295
  24. theorem OAI.CHObstruction.Arrays.RawEmbedding.index_exists line 304
  25. theorem OAI.CHObstruction.Arrays.RawEmbedding.base_exists line 308
  26. def OAI.CHObstruction.Arrays.RawEmbedding.index line 312
  27. def OAI.CHObstruction.Arrays.RawEmbedding.base line 314
  28. theorem OAI.CHObstruction.Arrays.RawEmbedding.index_apply line 316
  29. theorem OAI.CHObstruction.Arrays.RawEmbedding.base_apply line 319
  30. def OAI.CHObstruction.Arrays.RawEmbedding.indexEmb line 322
  31. def OAI.CHObstruction.Arrays.RawEmbedding.baseEmb line 326
  32. theorem OAI.CHObstruction.Arrays.RawEmbedding.indexEmb_apply line 331
  33. theorem OAI.CHObstruction.Arrays.RawEmbedding.baseEmb_apply line 332
  34. theorem OAI.CHObstruction.Arrays.RawEmbedding.group_apply line 334
  35. theorem OAI.CHObstruction.Arrays.RawEmbedding.star_apply line 346
  36. theorem OAI.CHObstruction.Arrays.RawEmbedding.row_exists line 352
  37. theorem OAI.CHObstruction.Arrays.RawEmbedding.col_exists line 369
  38. def OAI.CHObstruction.Arrays.RawEmbedding.rowShift line 386
  39. def OAI.CHObstruction.Arrays.RawEmbedding.colShift line 389
  40. theorem OAI.CHObstruction.Arrays.RawEmbedding.row_zero line 392
  41. theorem OAI.CHObstruction.Arrays.RawEmbedding.col_zero line 396
  42. theorem OAI.CHObstruction.Arrays.RawEmbedding.row_apply line 400
  43. theorem OAI.CHObstruction.Arrays.RawEmbedding.col_apply line 410
  44. def OAI.CHObstruction.Arrays.RawEmbedding.toMap line 420
  45. theorem OAI.CHObstruction.Arrays.RawEmbedding.toMap_onPoint line 433