OAI/Geometry/Borsuk/FiniteCases/Cases066.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c25388 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c25408 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c25430 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c25474 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c25523 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c25579 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c25590 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c25603 line 79
  9. theorem OAI.BorsukNine.FiniteObstruction.c25604 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c25607 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c25613 line 103
  12. theorem OAI.BorsukNine.FiniteObstruction.c25616 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c25617 line 119
  14. theorem OAI.BorsukNine.FiniteObstruction.c25618 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c25619 line 135
  16. theorem OAI.BorsukNine.FiniteObstruction.c25621 line 143
  17. theorem OAI.BorsukNine.FiniteObstruction.c25625 line 151
  18. theorem OAI.BorsukNine.FiniteObstruction.c25635 line 161
  19. theorem OAI.BorsukNine.FiniteObstruction.c25643 line 171
  20. theorem OAI.BorsukNine.FiniteObstruction.c25652 line 181
  21. theorem OAI.BorsukNine.FiniteObstruction.c25663 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c25667 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c25668 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c25702 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c25704 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c25708 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c25728 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c25730 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c25735 line 271
  30. theorem OAI.BorsukNine.FiniteObstruction.c25738 line 281
  31. theorem OAI.BorsukNine.FiniteObstruction.c25740 line 291
  32. theorem OAI.BorsukNine.FiniteObstruction.c25756 line 301
  33. theorem OAI.BorsukNine.FiniteObstruction.c25805 line 309
  34. theorem OAI.BorsukNine.FiniteObstruction.c25807 line 319
  35. theorem OAI.BorsukNine.FiniteObstruction.c25859 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c25883 line 339
  37. theorem OAI.BorsukNine.FiniteObstruction.c25885 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c25900 line 355
  39. theorem OAI.BorsukNine.FiniteObstruction.c26016 line 363
  40. theorem OAI.BorsukNine.FiniteObstruction.c26018 line 373
  41. theorem OAI.BorsukNine.FiniteObstruction.c26023 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c26031 line 391
  43. theorem OAI.BorsukNine.FiniteObstruction.c26038 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c26039 line 407
  45. theorem OAI.BorsukNine.FiniteObstruction.c26045 line 415
  46. theorem OAI.BorsukNine.FiniteObstruction.c26047 line 425