OAI/Geometry/Borsuk/FiniteCases/Cases037.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c10366 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c10379 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c10411 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c10421 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c10435 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c10455 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c10482 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c10484 line 79
  9. theorem OAI.BorsukNine.FiniteObstruction.c10485 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c10486 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c10493 line 103
  12. theorem OAI.BorsukNine.FiniteObstruction.c10499 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c10519 line 119
  14. theorem OAI.BorsukNine.FiniteObstruction.c10583 line 129
  15. theorem OAI.BorsukNine.FiniteObstruction.c10585 line 139
  16. theorem OAI.BorsukNine.FiniteObstruction.c10587 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c10608 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c10623 line 169
  19. theorem OAI.BorsukNine.FiniteObstruction.c10626 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c10627 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c10635 line 193
  22. theorem OAI.BorsukNine.FiniteObstruction.c10636 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c10637 line 209
  24. theorem OAI.BorsukNine.FiniteObstruction.c10638 line 217
  25. theorem OAI.BorsukNine.FiniteObstruction.c10691 line 225
  26. theorem OAI.BorsukNine.FiniteObstruction.c10693 line 235
  27. theorem OAI.BorsukNine.FiniteObstruction.c10715 line 245
  28. theorem OAI.BorsukNine.FiniteObstruction.c10717 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c10718 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c10719 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c10725 line 285
  32. theorem OAI.BorsukNine.FiniteObstruction.c10727 line 295
  33. theorem OAI.BorsukNine.FiniteObstruction.c10743 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c10744 line 315
  35. theorem OAI.BorsukNine.FiniteObstruction.c10751 line 325
  36. theorem OAI.BorsukNine.FiniteObstruction.c10763 line 335
  37. theorem OAI.BorsukNine.FiniteObstruction.c10778 line 343
  38. theorem OAI.BorsukNine.FiniteObstruction.c10780 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c10785 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c10793 line 369
  41. theorem OAI.BorsukNine.FiniteObstruction.c10795 line 379
  42. theorem OAI.BorsukNine.FiniteObstruction.c10817 line 389
  43. theorem OAI.BorsukNine.FiniteObstruction.c10827 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c10833 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c10849 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c10851 line 429