OAI/ModelTheory/Categoricity/Diagrams.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CHObstruction.Diagrams.Tag line 15
  2. def OAI.CHObstruction.Diagrams.tagOrdinal line 17
  3. theorem OAI.CHObstruction.Diagrams.tag_lt line 19
  4. abbrev OAI.CHObstruction.Diagrams.Label line 21
  5. def OAI.CHObstruction.Diagrams.Label.map line 25
  6. def OAI.CHObstruction.Diagrams.Label.root line 28
  7. theorem OAI.CHObstruction.Diagrams.Label.map_refl line 30
  8. theorem OAI.CHObstruction.Diagrams.Label.map_comp line 35
  9. theorem OAI.CHObstruction.Diagrams.Label.map_root line 40
  10. def OAI.CHObstruction.Diagrams.Label.congr line 44
  11. structure OAI.CHObstruction.Diagrams.Diagram line 60
  12. structure OAI.CHObstruction.Diagrams.Diagram.Valid line 69
  13. def OAI.CHObstruction.Diagrams.Diagram.restrict line 77
  14. theorem OAI.CHObstruction.Diagrams.Diagram.restrict_refl line 82
  15. theorem OAI.CHObstruction.Diagrams.Diagram.restrict_comp line 87
  16. theorem OAI.CHObstruction.Diagrams.Diagram.valid_restrict_equiv line 91
  17. def OAI.CHObstruction.Diagrams.Diagram.setoid line 112
  18. abbrev OAI.CHObstruction.Diagrams.Diagram.Q line 116
  19. def OAI.CHObstruction.Diagrams.Diagram.qRel line 118
  20. def OAI.CHObstruction.Diagrams.Diagram.qTag line 121
  21. theorem OAI.CHObstruction.Diagrams.Diagram.q_extensional line 125
  22. theorem OAI.CHObstruction.Diagrams.Diagram.q_decreases line 133
  23. theorem OAI.CHObstruction.Diagrams.Diagram.q_bound line 139
  24. def OAI.CHObstruction.Diagrams.Diagram.qMap line 145
  25. theorem OAI.CHObstruction.Diagrams.Diagram.qMap_mk line 163
  26. def OAI.CHObstruction.NoPattern.inclusion line 183
  27. def OAI.CHObstruction.NoPattern.positions line 188
  28. def OAI.CHObstruction.NoPattern.stage line 192
  29. theorem OAI.CHObstruction.NoPattern.stage_valid line 196
  30. theorem OAI.CHObstruction.NoPattern.stage_restrict line 200
  31. abbrev OAI.CHObstruction.NoPattern.F line 210
  32. def OAI.CHObstruction.NoPattern.transition line 212
  33. instance OAI.CHObstruction.NoPattern.directedSystem line 216
  34. def OAI.CHObstruction.NoPattern.stageRelation line 233
  35. def OAI.CHObstruction.NoPattern.stageTag line 236
  36. theorem OAI.CHObstruction.NoPattern.relation_compatible line 239
  37. theorem OAI.CHObstruction.NoPattern.tag_compatible line 250
  38. abbrev OAI.CHObstruction.NoPattern.Limit line 259
  39. def OAI.CHObstruction.NoPattern.root line 261
  40. theorem OAI.CHObstruction.NoPattern.root_injective line 264
  41. def OAI.CHObstruction.NoPattern.rootsEmbedding line 272
  42. theorem OAI.CHObstruction.NoPattern.impossible line 285