OAI/Geometry/Borsuk/FiniteCases/Cases007.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c585 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c587 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c588 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c589 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c590 line 55
  6. theorem OAI.BorsukNine.FiniteObstruction.c592 line 60
  7. theorem OAI.BorsukNine.FiniteObstruction.c593 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c594 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c595 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c596 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c599 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c600 line 126
  13. theorem OAI.BorsukNine.FiniteObstruction.c601 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c602 line 148
  15. theorem OAI.BorsukNine.FiniteObstruction.c603 line 165
  16. theorem OAI.BorsukNine.FiniteObstruction.c605 line 170
  17. theorem OAI.BorsukNine.FiniteObstruction.c607 line 175
  18. theorem OAI.BorsukNine.FiniteObstruction.c609 line 180
  19. theorem OAI.BorsukNine.FiniteObstruction.c611 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c615 line 190
  21. theorem OAI.BorsukNine.FiniteObstruction.c616 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c617 line 212
  23. theorem OAI.BorsukNine.FiniteObstruction.c618 line 229
  24. theorem OAI.BorsukNine.FiniteObstruction.c620 line 234
  25. theorem OAI.BorsukNine.FiniteObstruction.c626 line 239
  26. theorem OAI.BorsukNine.FiniteObstruction.c630 line 244
  27. theorem OAI.BorsukNine.FiniteObstruction.c632 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c633 line 266
  29. theorem OAI.BorsukNine.FiniteObstruction.c634 line 271
  30. theorem OAI.BorsukNine.FiniteObstruction.c635 line 288
  31. theorem OAI.BorsukNine.FiniteObstruction.c636 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c637 line 310
  33. theorem OAI.BorsukNine.FiniteObstruction.c638 line 315
  34. theorem OAI.BorsukNine.FiniteObstruction.c640 line 332
  35. theorem OAI.BorsukNine.FiniteObstruction.c641 line 349
  36. theorem OAI.BorsukNine.FiniteObstruction.c643 line 354
  37. theorem OAI.BorsukNine.FiniteObstruction.c644 line 359
  38. theorem OAI.BorsukNine.FiniteObstruction.c646 line 376
  39. theorem OAI.BorsukNine.FiniteObstruction.c647 line 393
  40. theorem OAI.BorsukNine.FiniteObstruction.c648 line 410
  41. theorem OAI.BorsukNine.FiniteObstruction.c650 line 415
  42. theorem OAI.BorsukNine.FiniteObstruction.c651 line 420