OAI/ModelTheory/Categoricity/Arrays.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CHObstruction.Matrix.bit line 21
  2. theorem OAI.CHObstruction.Matrix.decompose line 24
  3. theorem OAI.CHObstruction.Matrix.normalize line 45
  4. inductive OAI.CHObstruction.Arrays.Point line 61
  5. inductive OAI.CHObstruction.Arrays.Symbol line 69
  6. def OAI.CHObstruction.Arrays.Symbol.arity line 77
  7. def OAI.CHObstruction.Arrays.Language line 84
  8. instance OAI.CHObstruction.Arrays.language_countable line 86
  9. structure OAI.CHObstruction.Arrays.Data line 96
  10. abbrev OAI.CHObstruction.Arrays.Data.Carrier line 110
  11. def OAI.CHObstruction.Arrays.Data.rawRel line 116
  12. def OAI.CHObstruction.Arrays.Data.rel line 137
  13. def OAI.CHObstruction.Arrays.Data.colors line 140
  14. def OAI.CHObstruction.Arrays.Data.IsObject line 143
  15. theorem OAI.CHObstruction.Arrays.Data.countable_object line 146
  16. theorem OAI.CHObstruction.Arrays.Data.base_bound line 149
  17. theorem OAI.CHObstruction.Arrays.Data.uncountable_index_bound line 152
  18. def OAI.CHObstruction.Tuples.map line 162
  19. theorem OAI.CHObstruction.Tuples.map_fst line 164
  20. theorem OAI.CHObstruction.Tuples.map_injective line 166
  21. theorem OAI.CHObstruction.Tuples.map_refl line 175
  22. theorem OAI.CHObstruction.Tuples.map_comp line 179
  23. theorem OAI.CHObstruction.Tuples.map_sub line 182
  24. theorem OAI.CHObstruction.Tuples.cardinal_bound line 185
  25. theorem OAI.CHObstruction.FiniteSupports.map_symmDiff line 210
  26. theorem OAI.CHObstruction.FiniteSupports.bit_symmDiff line 223
  27. theorem OAI.CHObstruction.FiniteSupports.bit_map line 228
  28. structure OAI.CHObstruction.Arrays.Map line 243
  29. def OAI.CHObstruction.Arrays.Map.onPoint line 251
  30. theorem OAI.CHObstruction.Arrays.Map.injective line 259
  31. def OAI.CHObstruction.Arrays.Map.toEmbedding line 278
  32. theorem OAI.CHObstruction.Arrays.Map.base_embedding_apply line 281
  33. theorem OAI.CHObstruction.Arrays.Map.bit_all line 284
  34. theorem OAI.CHObstruction.Tuples.map_eq_iff line 304