OAI/Geometry/Borsuk/FiniteCases/Cases027.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c4147 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c4163 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c4164 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c4191 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c4195 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c4213 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c4326 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c4328 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c4333 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c4389 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c4455 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c4468 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c4471 line 119
  14. theorem OAI.BorsukNine.FiniteObstruction.c4479 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c4481 line 135
  16. theorem OAI.BorsukNine.FiniteObstruction.c4521 line 143
  17. theorem OAI.BorsukNine.FiniteObstruction.c4584 line 153
  18. theorem OAI.BorsukNine.FiniteObstruction.c4604 line 163
  19. theorem OAI.BorsukNine.FiniteObstruction.c4605 line 171
  20. theorem OAI.BorsukNine.FiniteObstruction.c4607 line 179
  21. theorem OAI.BorsukNine.FiniteObstruction.c4609 line 187
  22. theorem OAI.BorsukNine.FiniteObstruction.c4611 line 195
  23. theorem OAI.BorsukNine.FiniteObstruction.c4621 line 203
  24. theorem OAI.BorsukNine.FiniteObstruction.c4638 line 211
  25. theorem OAI.BorsukNine.FiniteObstruction.c4657 line 221
  26. theorem OAI.BorsukNine.FiniteObstruction.c4682 line 231
  27. theorem OAI.BorsukNine.FiniteObstruction.c4685 line 241
  28. theorem OAI.BorsukNine.FiniteObstruction.c4689 line 251
  29. theorem OAI.BorsukNine.FiniteObstruction.c4694 line 261
  30. theorem OAI.BorsukNine.FiniteObstruction.c4695 line 271
  31. theorem OAI.BorsukNine.FiniteObstruction.c4699 line 281
  32. theorem OAI.BorsukNine.FiniteObstruction.c4700 line 291
  33. theorem OAI.BorsukNine.FiniteObstruction.c4707 line 301
  34. theorem OAI.BorsukNine.FiniteObstruction.c4708 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c4709 line 321
  36. theorem OAI.BorsukNine.FiniteObstruction.c4717 line 331
  37. theorem OAI.BorsukNine.FiniteObstruction.c4719 line 341
  38. theorem OAI.BorsukNine.FiniteObstruction.c4725 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c4730 line 361
  40. theorem OAI.BorsukNine.FiniteObstruction.c4733 line 371
  41. theorem OAI.BorsukNine.FiniteObstruction.c4736 line 381
  42. theorem OAI.BorsukNine.FiniteObstruction.c4751 line 391
  43. theorem OAI.BorsukNine.FiniteObstruction.c4865 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c4882 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c4891 line 417
  46. theorem OAI.BorsukNine.FiniteObstruction.c4895 line 425