OAI/Geometry/Borsuk/FiniteCases/Cases107.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c31899 line 23
  2. theorem OAI.BorsukNine.FiniteObstruction.c31900 line 32
  3. theorem OAI.BorsukNine.FiniteObstruction.c31905 line 41
  4. theorem OAI.BorsukNine.FiniteObstruction.c31906 line 50
  5. theorem OAI.BorsukNine.FiniteObstruction.c31917 line 59
  6. theorem OAI.BorsukNine.FiniteObstruction.c31918 line 68
  7. theorem OAI.BorsukNine.FiniteObstruction.c31919 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c31920 line 86
  9. theorem OAI.BorsukNine.FiniteObstruction.c31923 line 95
  10. theorem OAI.BorsukNine.FiniteObstruction.c31926 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c31929 line 113
  12. theorem OAI.BorsukNine.FiniteObstruction.c31930 line 122
  13. theorem OAI.BorsukNine.FiniteObstruction.c31947 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c31957 line 140
  15. theorem OAI.BorsukNine.FiniteObstruction.c31967 line 149
  16. theorem OAI.BorsukNine.FiniteObstruction.c31976 line 158
  17. theorem OAI.BorsukNine.FiniteObstruction.c31993 line 167
  18. theorem OAI.BorsukNine.FiniteObstruction.c32011 line 176
  19. theorem OAI.BorsukNine.FiniteObstruction.c32015 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c32016 line 194
  21. theorem OAI.BorsukNine.FiniteObstruction.c32025 line 203
  22. theorem OAI.BorsukNine.FiniteObstruction.c32033 line 212
  23. theorem OAI.BorsukNine.FiniteObstruction.c32047 line 221
  24. theorem OAI.BorsukNine.FiniteObstruction.c32052 line 230
  25. theorem OAI.BorsukNine.FiniteObstruction.c32085 line 239
  26. theorem OAI.BorsukNine.FiniteObstruction.c32086 line 248
  27. theorem OAI.BorsukNine.FiniteObstruction.c32087 line 257
  28. theorem OAI.BorsukNine.FiniteObstruction.c32101 line 266
  29. theorem OAI.BorsukNine.FiniteObstruction.c32117 line 275
  30. theorem OAI.BorsukNine.FiniteObstruction.c32121 line 284
  31. theorem OAI.BorsukNine.FiniteObstruction.c32123 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c32126 line 302
  33. theorem OAI.BorsukNine.FiniteObstruction.c32137 line 311
  34. theorem OAI.BorsukNine.FiniteObstruction.c32147 line 320
  35. theorem OAI.BorsukNine.FiniteObstruction.c32148 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c32157 line 338
  37. theorem OAI.BorsukNine.FiniteObstruction.c32166 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c32167 line 356
  39. theorem OAI.BorsukNine.FiniteObstruction.c32176 line 365
  40. theorem OAI.BorsukNine.FiniteObstruction.c32182 line 374
  41. theorem OAI.BorsukNine.FiniteObstruction.c32192 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c32193 line 392
  43. theorem OAI.BorsukNine.FiniteObstruction.c32197 line 401
  44. theorem OAI.BorsukNine.FiniteObstruction.c32207 line 410
  45. theorem OAI.BorsukNine.FiniteObstruction.c32209 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c32210 line 428
  47. theorem OAI.BorsukNine.FiniteObstruction.c32211 line 437