OAI/ModelTheory/Categoricity/EndpointDiagrams.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CHObstruction.EndpointDiagrams.V line 17
  2. abbrev OAI.CHObstruction.EndpointDiagrams.D line 18
  3. def OAI.CHObstruction.EndpointDiagrams.element line 20
  4. def OAI.CHObstruction.EndpointDiagrams.membership line 22
  5. theorem OAI.CHObstruction.EndpointDiagrams.separates line 24
  6. def OAI.CHObstruction.EndpointDiagrams.rank line 31
  7. def OAI.CHObstruction.EndpointDiagrams.seed line 34
  8. def OAI.CHObstruction.EndpointDiagrams.fullSeed line 37
  9. def OAI.CHObstruction.EndpointDiagrams.entry line 39
  10. theorem OAI.CHObstruction.EndpointDiagrams.entry_mem line 42
  11. theorem OAI.CHObstruction.EndpointDiagrams.entry_surjective line 48
  12. theorem OAI.CHObstruction.EndpointDiagrams.entry_root line 53
  13. theorem OAI.CHObstruction.EndpointDiagrams.entry_comp line 62
  14. def OAI.CHObstruction.EndpointDiagrams.beta line 71
  15. def OAI.CHObstruction.EndpointDiagrams.localTag line 73
  16. theorem OAI.CHObstruction.EndpointDiagrams.localTag_value line 76
  17. def OAI.CHObstruction.EndpointDiagrams.diagram line 80
  18. theorem OAI.CHObstruction.EndpointDiagrams.diagram_restrict line 85
  19. def OAI.CHObstruction.EndpointDiagrams.Good line 93
  20. theorem OAI.CHObstruction.EndpointDiagrams.countable_bad line 97
  21. theorem OAI.CHObstruction.EndpointDiagrams.good_mono line 120
  22. theorem OAI.CHObstruction.EndpointDiagrams.diagram_valid line 126
  23. theorem OAI.CHObstruction.EndpointDiagrams.sub_seed line 148
  24. def OAI.CHObstruction.EndpointDiagrams.colors line 154
  25. theorem OAI.CHObstruction.EndpointDiagrams.passes line 157
  26. theorem OAI.CHObstruction.EndpointDiagrams.countable_failures line 164
  27. theorem OAI.CHObstruction.EndpointDiagrams.cardinal line 168