OAI/Geometry/Borsuk/FiniteCases/Cases057.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c20427 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c20431 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c20434 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c20436 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c20437 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c20445 line 51
  7. theorem OAI.BorsukNine.FiniteObstruction.c20448 line 61
  8. theorem OAI.BorsukNine.FiniteObstruction.c20451 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c20475 line 81
  10. theorem OAI.BorsukNine.FiniteObstruction.c20479 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c20483 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c20500 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c20507 line 121
  14. theorem OAI.BorsukNine.FiniteObstruction.c20510 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c20563 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c20567 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c20571 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c20575 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c20581 line 173
  20. theorem OAI.BorsukNine.FiniteObstruction.c20623 line 181
  21. theorem OAI.BorsukNine.FiniteObstruction.c20630 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c20679 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c20698 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c20700 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c20703 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c20704 line 239
  27. theorem OAI.BorsukNine.FiniteObstruction.c20705 line 247
  28. theorem OAI.BorsukNine.FiniteObstruction.c20707 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c20709 line 263
  30. theorem OAI.BorsukNine.FiniteObstruction.c20713 line 271
  31. theorem OAI.BorsukNine.FiniteObstruction.c20716 line 279
  32. theorem OAI.BorsukNine.FiniteObstruction.c20717 line 287
  33. theorem OAI.BorsukNine.FiniteObstruction.c20718 line 295
  34. theorem OAI.BorsukNine.FiniteObstruction.c20719 line 303
  35. theorem OAI.BorsukNine.FiniteObstruction.c20720 line 311
  36. theorem OAI.BorsukNine.FiniteObstruction.c20721 line 319
  37. theorem OAI.BorsukNine.FiniteObstruction.c20727 line 327
  38. theorem OAI.BorsukNine.FiniteObstruction.c20731 line 337
  39. theorem OAI.BorsukNine.FiniteObstruction.c20735 line 347
  40. theorem OAI.BorsukNine.FiniteObstruction.c20743 line 357
  41. theorem OAI.BorsukNine.FiniteObstruction.c20752 line 367
  42. theorem OAI.BorsukNine.FiniteObstruction.c20763 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c20767 line 387
  44. theorem OAI.BorsukNine.FiniteObstruction.c20768 line 397
  45. theorem OAI.BorsukNine.FiniteObstruction.c20772 line 407
  46. theorem OAI.BorsukNine.FiniteObstruction.c20804 line 417
  47. theorem OAI.BorsukNine.FiniteObstruction.c20808 line 427