OAI/Geometry/Borsuk/FiniteCases/Cases070.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c27508 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c27540 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c27548 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c27550 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c27563 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c27566 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c27569 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c27571 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c27572 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c27573 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c27575 line 99
  12. theorem OAI.BorsukNine.FiniteObstruction.c27578 line 107
  13. theorem OAI.BorsukNine.FiniteObstruction.c27580 line 115
  14. theorem OAI.BorsukNine.FiniteObstruction.c27581 line 123
  15. theorem OAI.BorsukNine.FiniteObstruction.c27587 line 131
  16. theorem OAI.BorsukNine.FiniteObstruction.c27588 line 141
  17. theorem OAI.BorsukNine.FiniteObstruction.c27595 line 151
  18. theorem OAI.BorsukNine.FiniteObstruction.c27621 line 161
  19. theorem OAI.BorsukNine.FiniteObstruction.c27623 line 171
  20. theorem OAI.BorsukNine.FiniteObstruction.c27628 line 181
  21. theorem OAI.BorsukNine.FiniteObstruction.c27640 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c27667 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c27675 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c27680 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c27682 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c27695 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c27703 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c27704 line 259
  29. theorem OAI.BorsukNine.FiniteObstruction.c27710 line 267
  30. theorem OAI.BorsukNine.FiniteObstruction.c27718 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c27720 line 283
  32. theorem OAI.BorsukNine.FiniteObstruction.c27721 line 291
  33. theorem OAI.BorsukNine.FiniteObstruction.c27765 line 299
  34. theorem OAI.BorsukNine.FiniteObstruction.c27827 line 309
  35. theorem OAI.BorsukNine.FiniteObstruction.c27838 line 319
  36. theorem OAI.BorsukNine.FiniteObstruction.c27843 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c27849 line 337
  38. theorem OAI.BorsukNine.FiniteObstruction.c27854 line 345
  39. theorem OAI.BorsukNine.FiniteObstruction.c27855 line 353
  40. theorem OAI.BorsukNine.FiniteObstruction.c27856 line 361
  41. theorem OAI.BorsukNine.FiniteObstruction.c27857 line 369
  42. theorem OAI.BorsukNine.FiniteObstruction.c27858 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c27859 line 385
  44. theorem OAI.BorsukNine.FiniteObstruction.c27860 line 393
  45. theorem OAI.BorsukNine.FiniteObstruction.c27863 line 401
  46. theorem OAI.BorsukNine.FiniteObstruction.c27865 line 411
  47. theorem OAI.BorsukNine.FiniteObstruction.c27871 line 421