OAI/Geometry/Borsuk/FiniteCases/Cases012.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c993 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c995 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c996 line 21
  4. theorem OAI.BorsukNine.FiniteObstruction.c997 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c999 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c1001 line 48
  7. theorem OAI.BorsukNine.FiniteObstruction.c1006 line 53
  8. theorem OAI.BorsukNine.FiniteObstruction.c1008 line 70
  9. theorem OAI.BorsukNine.FiniteObstruction.c1010 line 75
  10. theorem OAI.BorsukNine.FiniteObstruction.c1012 line 80
  11. theorem OAI.BorsukNine.FiniteObstruction.c1016 line 85
  12. theorem OAI.BorsukNine.FiniteObstruction.c1020 line 90
  13. theorem OAI.BorsukNine.FiniteObstruction.c1022 line 95
  14. theorem OAI.BorsukNine.FiniteObstruction.c1025 line 112
  15. theorem OAI.BorsukNine.FiniteObstruction.c1029 line 117
  16. theorem OAI.BorsukNine.FiniteObstruction.c1030 line 122
  17. theorem OAI.BorsukNine.FiniteObstruction.c1035 line 139
  18. theorem OAI.BorsukNine.FiniteObstruction.c1037 line 144
  19. theorem OAI.BorsukNine.FiniteObstruction.c1038 line 161
  20. theorem OAI.BorsukNine.FiniteObstruction.c1040 line 166
  21. theorem OAI.BorsukNine.FiniteObstruction.c1042 line 171
  22. theorem OAI.BorsukNine.FiniteObstruction.c1043 line 176
  23. theorem OAI.BorsukNine.FiniteObstruction.c1044 line 193
  24. theorem OAI.BorsukNine.FiniteObstruction.c1047 line 198
  25. theorem OAI.BorsukNine.FiniteObstruction.c1049 line 215
  26. theorem OAI.BorsukNine.FiniteObstruction.c1050 line 232
  27. theorem OAI.BorsukNine.FiniteObstruction.c1053 line 237
  28. theorem OAI.BorsukNine.FiniteObstruction.c1059 line 242
  29. theorem OAI.BorsukNine.FiniteObstruction.c1063 line 247
  30. theorem OAI.BorsukNine.FiniteObstruction.c1067 line 252
  31. theorem OAI.BorsukNine.FiniteObstruction.c1073 line 269
  32. theorem OAI.BorsukNine.FiniteObstruction.c1076 line 286
  33. theorem OAI.BorsukNine.FiniteObstruction.c1077 line 291
  34. theorem OAI.BorsukNine.FiniteObstruction.c1078 line 308
  35. theorem OAI.BorsukNine.FiniteObstruction.c1082 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c1091 line 330
  37. theorem OAI.BorsukNine.FiniteObstruction.c1092 line 335
  38. theorem OAI.BorsukNine.FiniteObstruction.c1095 line 352
  39. theorem OAI.BorsukNine.FiniteObstruction.c1096 line 357
  40. theorem OAI.BorsukNine.FiniteObstruction.c1097 line 374
  41. theorem OAI.BorsukNine.FiniteObstruction.c1111 line 391
  42. theorem OAI.BorsukNine.FiniteObstruction.c1112 line 408
  43. theorem OAI.BorsukNine.FiniteObstruction.c1113 line 425