OAI/ModelTheory/Categoricity/AEC.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CHObstruction.RelModel.Iso.refl line 17
  2. def OAI.CHObstruction.RelModel.Iso.symm line 19
  3. def OAI.CHObstruction.RelModel.Iso.trans line 25
  4. theorem OAI.CHObstruction.RelModel.IsSubstructure.antisymm line 29
  5. theorem OAI.CHObstruction.Arrays.Data.rawRel_length line 46
  6. def OAI.CHObstruction.Arrays.rawIsoOfTyped line 51
  7. structure OAI.CHObstruction.Arrays.Presentation line 64
  8. def OAI.CHObstruction.Arrays.Presentation.transport line 73
  9. theorem OAI.CHObstruction.Arrays.Presentation.relates_symm line 78
  10. def OAI.CHObstruction.Arrays.Presentation.comparison line 82
  11. theorem OAI.CHObstruction.Arrays.Presentation.comparison_onPoint line 87
  12. theorem OAI.CHObstruction.Arrays.Presentation.comparison_strong line 91
  13. theorem OAI.CHObstruction.Arrays.Presentation.object_iff line 95
  14. def OAI.CHObstruction.Arrays.Presentation.isoOfMap line 105
  15. def OAI.CHObstruction.Arrays.Presentation.Inclusion line 112
  16. theorem OAI.CHObstruction.Arrays.Presentation.inclusion_unique line 115
  17. theorem OAI.CHObstruction.Arrays.Presentation.inclusion_refl line 123
  18. theorem OAI.CHObstruction.Arrays.Presentation.Inclusion.comp line 127
  19. theorem OAI.CHObstruction.Arrays.Presentation.inclusion_comparison line 134
  20. theorem OAI.CHObstruction.Arrays.Presentation.Inclusion.substructure line 138
  21. def OAI.CHObstruction.Arrays.classData line 158
  22. abbrev OAI.CHObstruction.Arrays.AEC.Object line 168
  23. abbrev OAI.CHObstruction.Arrays.AEC.Strong line 169
  24. theorem OAI.CHObstruction.Arrays.AEC.strong_objects line 171
  25. theorem OAI.CHObstruction.Arrays.AEC.object_presentation line 175
  26. theorem OAI.CHObstruction.Arrays.AEC.strong_rebase line 179
  27. theorem OAI.CHObstruction.Arrays.AEC.strong_of line 186
  28. theorem OAI.CHObstruction.Arrays.AEC.refl line 191
  29. theorem OAI.CHObstruction.Arrays.AEC.substructure line 195
  30. theorem OAI.CHObstruction.Arrays.AEC.antisymm line 199
  31. theorem OAI.CHObstruction.Arrays.AEC.trans line 202
  32. theorem OAI.CHObstruction.Arrays.AEC.iso_objects line 208
  33. theorem OAI.CHObstruction.Arrays.AEC.iso_strong line 212
  34. theorem OAI.CHObstruction.Arrays.AEC.coherence line 225
  35. theorem OAI.CHObstruction.Arrays.Coding.cardinal line 249
  36. def OAI.CHObstruction.Arrays.Coding.universeEquiv line 253
  37. def OAI.CHObstruction.Arrays.Coding.rangeEquiv line 257
  38. def OAI.CHObstruction.Arrays.Coding.model line 264
  39. def OAI.CHObstruction.Arrays.Coding.presentation line 268
  40. def OAI.CHObstruction.Arrays.Coding.coded line 275
  41. def OAI.CHObstruction.Arrays.Coding.codedPresentation line 277
  42. theorem OAI.CHObstruction.Arrays.Coding.coded_cardinal line 280
  43. theorem OAI.CHObstruction.Arrays.AEC.small line 291
  44. theorem OAI.CHObstruction.Arrays.AEC.directed_union line 327
  45. theorem OAI.CHObstruction.Arrays.AEC.lsBound line 404
  46. theorem OAI.CHObstruction.Arrays.AEC.isAEC line 409
  47. theorem OAI.CHObstruction.Arrays.AEC.hasLSNumber line 423