OAI/ModelTheory/Categoricity/DirectedLimits.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

Directed limits of finite-support arrays

The index, base and six-sorted carrier are constructed as directed limits. Finite tuples and supports can be represented in a common stage. Compatible row and column actions give the limit its relational interpretation, and convexity supplies local countability and the strong-embedding properties.

  1. abbrev OAI.CHObstruction.LimitTools.Limit line 28
  2. def OAI.CHObstruction.LimitTools.of line 30
  3. theorem OAI.CHObstruction.LimitTools.of_map line 33
  4. theorem OAI.CHObstruction.LimitTools.common line 37
  5. structure OAI.CHObstruction.Arrays.System.Data line 57
  6. def OAI.CHObstruction.Arrays.System.Data.indexMap line 70
  7. def OAI.CHObstruction.Arrays.System.Data.baseMap line 72
  8. def OAI.CHObstruction.Arrays.System.Data.pointMap line 74
  9. instance OAI.CHObstruction.Arrays.System.Data.indexSystem line 77
  10. instance OAI.CHObstruction.Arrays.System.Data.baseSystem line 83
  11. instance OAI.CHObstruction.Arrays.System.Data.pointSystem line 89
  12. abbrev OAI.CHObstruction.Arrays.System.Data.I line 97
  13. abbrev OAI.CHObstruction.Arrays.System.Data.B line 98
  14. abbrev OAI.CHObstruction.Arrays.System.Data.X line 99
  15. def OAI.CHObstruction.Arrays.System.Data.index line 101
  16. def OAI.CHObstruction.Arrays.System.Data.base line 104
  17. def OAI.CHObstruction.Arrays.System.Data.point line 107
  18. theorem OAI.CHObstruction.Arrays.System.Data.index_map line 111
  19. theorem OAI.CHObstruction.Arrays.System.Data.base_map line 115
  20. theorem OAI.CHObstruction.Arrays.System.Data.point_map line 119
  21. instance OAI.CHObstruction.Arrays.System.Data.(instance at line 122) line 122
  22. instance OAI.CHObstruction.Arrays.System.Data.(instance at line 123) line 123
  23. def OAI.CHObstruction.Arrays.System.Data.le line 125
  24. theorem OAI.CHObstruction.Arrays.System.Data.le_base line 129
  25. instance OAI.CHObstruction.Arrays.System.Data.leInstance line 134
  26. instance OAI.CHObstruction.Arrays.System.Data.ltInstance line 135
  27. instance OAI.CHObstruction.Arrays.System.Data.order line 137
  28. instance OAI.CHObstruction.Arrays.System.Data.preorder line 164
  29. def OAI.CHObstruction.Arrays.System.Data.baseOrder line 166
  30. theorem OAI.CHObstruction.Arrays.System.Data.tuple_map line 173
  31. theorem OAI.CHObstruction.Arrays.System.Data.finset_map line 181
  32. theorem OAI.CHObstruction.Arrays.System.Data.tuple_exists line 188
  33. theorem OAI.CHObstruction.Arrays.System.Data.finset_exists line 203
  34. def OAI.CHObstruction.Arrays.System.Data.shapeAt line 224
  35. theorem OAI.CHObstruction.Arrays.System.Data.shapeAt_map line 233
  36. def OAI.CHObstruction.Arrays.System.Data.shape line 237
  37. theorem OAI.CHObstruction.Arrays.System.Data.shape_point line 241
  38. def OAI.CHObstruction.Arrays.System.Data.rowDiffAt line 244
  39. def OAI.CHObstruction.Arrays.System.Data.colDiffAt line 248
  40. theorem OAI.CHObstruction.Arrays.System.Data.rowDiffAt_map line 253
  41. theorem OAI.CHObstruction.Arrays.System.Data.colDiffAt_map line 269
  42. def OAI.CHObstruction.Arrays.System.Data.rowDiff line 283
  43. def OAI.CHObstruction.Arrays.System.Data.colDiff line 286
  44. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_point line 290
  45. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_point line 295
  46. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_refl_at line 300
  47. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_refl_at line 306
  48. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_zero line 311
  49. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_zero line 328
  50. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_symm line 343
  51. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_symm line 354
  52. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_trans line 365
  53. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_trans line 391
  54. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_unique line 416
  55. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_unique line 423
  56. theorem OAI.CHObstruction.Arrays.System.Data.shapeAt_row line 431
  57. theorem OAI.CHObstruction.Arrays.System.Data.shapeAt_col line 441
  58. theorem OAI.CHObstruction.Arrays.System.Data.rowDiff_exists line 451
  59. theorem OAI.CHObstruction.Arrays.System.Data.colDiff_exists line 463
  60. theorem OAI.CHObstruction.Arrays.System.Data.base_lt line 476
  61. instance OAI.CHObstruction.Arrays.System.Data.dense line 481
  62. instance OAI.CHObstruction.Arrays.System.Data.noMin line 491
  63. instance OAI.CHObstruction.Arrays.System.Data.noMax line 499
  64. theorem OAI.CHObstruction.Arrays.System.Data.rowOrigin_exists line 507
  65. def OAI.CHObstruction.Arrays.System.Data.rowOrigin line 512
  66. theorem OAI.CHObstruction.Arrays.System.Data.rowOrigin_shape line 514
  67. theorem OAI.CHObstruction.Arrays.System.Data.colOrigin_exists line 517
  68. def OAI.CHObstruction.Arrays.System.Data.colOrigin line 527
  69. theorem OAI.CHObstruction.Arrays.System.Data.colOrigin_shape line 529
  70. theorem OAI.CHObstruction.Arrays.System.Data.row_translate_exists line 532
  71. theorem OAI.CHObstruction.Arrays.System.Data.col_translate_exists line 551
  72. def OAI.CHObstruction.Arrays.System.Data.rowPoint line 563
  73. def OAI.CHObstruction.Arrays.System.Data.colPoint line 566
  74. theorem OAI.CHObstruction.Arrays.System.Data.rowPoint_shape line 569
  75. theorem OAI.CHObstruction.Arrays.System.Data.rowPoint_diff line 573
  76. theorem OAI.CHObstruction.Arrays.System.Data.colPoint_shape line 577
  77. theorem OAI.CHObstruction.Arrays.System.Data.colPoint_diff line 581
  78. def OAI.CHObstruction.Arrays.System.Data.bitAt line 585
  79. theorem OAI.CHObstruction.Arrays.System.Data.bitAt_map line 590
  80. def OAI.CHObstruction.Arrays.System.Data.bit line 600
  81. theorem OAI.CHObstruction.Arrays.System.Data.bit_point line 604
  82. theorem OAI.CHObstruction.Arrays.System.Data.bit_row_change line 609
  83. theorem OAI.CHObstruction.Arrays.System.Data.bit_col_change line 636
  84. theorem OAI.CHObstruction.Arrays.System.Data.base_convex line 666
  85. theorem OAI.CHObstruction.Arrays.System.Data.locallyCountable line 687
  86. def OAI.CHObstruction.Arrays.System.Data.limitData line 697
  87. def OAI.CHObstruction.Arrays.System.Data.rowShift line 709
  88. def OAI.CHObstruction.Arrays.System.Data.colShift line 713
  89. theorem OAI.CHObstruction.Arrays.System.Data.rowShift_spec line 718
  90. theorem OAI.CHObstruction.Arrays.System.Data.colShift_spec line 724
  91. def OAI.CHObstruction.Arrays.System.Data.toLimit line 731
  92. theorem OAI.CHObstruction.Arrays.System.Data.rowShift_comp line 752
  93. theorem OAI.CHObstruction.Arrays.System.Data.colShift_comp line 768
  94. theorem OAI.CHObstruction.Arrays.System.Data.toLimit_comp line 785
  95. theorem OAI.CHObstruction.Arrays.System.Data.toLimit_covers line 816
  96. def OAI.CHObstruction.Arrays.System.Data.underlying line 854
  97. theorem OAI.CHObstruction.Arrays.System.Data.underlying_point line 860
  98. theorem OAI.CHObstruction.Arrays.System.Data.underlying_bijective line 863
  99. def OAI.CHObstruction.Arrays.System.Data.equivalence line 874
  100. theorem OAI.CHObstruction.Arrays.System.Data.equivalence_point line 877
  101. theorem OAI.CHObstruction.Arrays.System.Data.equivalence_symm_stage line 880
  102. theorem OAI.CHObstruction.Arrays.System.Data.common_points line 884
  103. theorem OAI.CHObstruction.Arrays.System.Data.toLimit_strong line 893
  104. theorem OAI.CHObstruction.Arrays.System.Data.limit_object line 918
  105. def OAI.CHObstruction.Arrays.System.Data.liftPoint line 945
  106. theorem OAI.CHObstruction.Arrays.System.Data.liftPoint_point line 950
  107. theorem OAI.CHObstruction.Arrays.System.Data.liftPoint_injective line 954
  108. def OAI.CHObstruction.Arrays.System.Data.liftFunction line 961
  109. theorem OAI.CHObstruction.Arrays.System.Data.liftFunction_stage line 964
  110. theorem OAI.CHObstruction.Arrays.System.Data.liftFunction_injective line 968
  111. def OAI.CHObstruction.Arrays.System.Data.liftRaw line 971
  112. def OAI.CHObstruction.Arrays.System.Data.liftMap line 1006
  113. theorem OAI.CHObstruction.Arrays.System.Data.liftMap_stage line 1008
  114. theorem OAI.CHObstruction.Arrays.System.Data.liftMap_comp line 1013
  115. theorem OAI.CHObstruction.Arrays.System.Data.liftMap_strong line 1021