OAI/Geometry/Borsuk/FiniteCases/Cases028.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c4939 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c4978 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c5003 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c5004 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c5005 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c5024 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c5028 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c5031 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c5089 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c5115 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c5137 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c5142 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c5171 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c5173 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c5179 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c5229 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c5255 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c5292 line 169
  19. theorem OAI.BorsukNine.FiniteObstruction.c5293 line 179
  20. theorem OAI.BorsukNine.FiniteObstruction.c5306 line 189
  21. theorem OAI.BorsukNine.FiniteObstruction.c5313 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c5369 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c5442 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c5449 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c5501 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c5509 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c5535 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c5571 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c5580 line 271
  30. theorem OAI.BorsukNine.FiniteObstruction.c5591 line 281
  31. theorem OAI.BorsukNine.FiniteObstruction.c5595 line 289
  32. theorem OAI.BorsukNine.FiniteObstruction.c5611 line 297
  33. theorem OAI.BorsukNine.FiniteObstruction.c5685 line 307
  34. theorem OAI.BorsukNine.FiniteObstruction.c5712 line 317
  35. theorem OAI.BorsukNine.FiniteObstruction.c5723 line 327
  36. theorem OAI.BorsukNine.FiniteObstruction.c5727 line 335
  37. theorem OAI.BorsukNine.FiniteObstruction.c5728 line 343
  38. theorem OAI.BorsukNine.FiniteObstruction.c5729 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c5731 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c5738 line 367
  41. theorem OAI.BorsukNine.FiniteObstruction.c5739 line 375
  42. theorem OAI.BorsukNine.FiniteObstruction.c5746 line 383
  43. theorem OAI.BorsukNine.FiniteObstruction.c5801 line 393
  44. theorem OAI.BorsukNine.FiniteObstruction.c5848 line 403
  45. theorem OAI.BorsukNine.FiniteObstruction.c5855 line 413
  46. theorem OAI.BorsukNine.FiniteObstruction.c5863 line 423