OAI/Geometry/Borsuk/FiniteCases/Cases044.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c13399 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c13407 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c13423 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c13425 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c13439 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c13455 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c13497 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c13562 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c13563 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c13566 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c13567 line 99
  12. theorem OAI.BorsukNine.FiniteObstruction.c13571 line 107
  13. theorem OAI.BorsukNine.FiniteObstruction.c13572 line 115
  14. theorem OAI.BorsukNine.FiniteObstruction.c13574 line 123
  15. theorem OAI.BorsukNine.FiniteObstruction.c13575 line 131
  16. theorem OAI.BorsukNine.FiniteObstruction.c13577 line 139
  17. theorem OAI.BorsukNine.FiniteObstruction.c13592 line 147
  18. theorem OAI.BorsukNine.FiniteObstruction.c13631 line 157
  19. theorem OAI.BorsukNine.FiniteObstruction.c13640 line 167
  20. theorem OAI.BorsukNine.FiniteObstruction.c13641 line 177
  21. theorem OAI.BorsukNine.FiniteObstruction.c13649 line 187
  22. theorem OAI.BorsukNine.FiniteObstruction.c13698 line 197
  23. theorem OAI.BorsukNine.FiniteObstruction.c13702 line 207
  24. theorem OAI.BorsukNine.FiniteObstruction.c13703 line 215
  25. theorem OAI.BorsukNine.FiniteObstruction.c13709 line 223
  26. theorem OAI.BorsukNine.FiniteObstruction.c13719 line 231
  27. theorem OAI.BorsukNine.FiniteObstruction.c13720 line 239
  28. theorem OAI.BorsukNine.FiniteObstruction.c13757 line 247
  29. theorem OAI.BorsukNine.FiniteObstruction.c13772 line 257
  30. theorem OAI.BorsukNine.FiniteObstruction.c13773 line 267
  31. theorem OAI.BorsukNine.FiniteObstruction.c13775 line 277
  32. theorem OAI.BorsukNine.FiniteObstruction.c13787 line 287
  33. theorem OAI.BorsukNine.FiniteObstruction.c13791 line 297
  34. theorem OAI.BorsukNine.FiniteObstruction.c13827 line 307
  35. theorem OAI.BorsukNine.FiniteObstruction.c13842 line 317
  36. theorem OAI.BorsukNine.FiniteObstruction.c13843 line 325
  37. theorem OAI.BorsukNine.FiniteObstruction.c13844 line 333
  38. theorem OAI.BorsukNine.FiniteObstruction.c13845 line 341
  39. theorem OAI.BorsukNine.FiniteObstruction.c13849 line 349
  40. theorem OAI.BorsukNine.FiniteObstruction.c13850 line 357
  41. theorem OAI.BorsukNine.FiniteObstruction.c13852 line 365
  42. theorem OAI.BorsukNine.FiniteObstruction.c13853 line 373
  43. theorem OAI.BorsukNine.FiniteObstruction.c13855 line 381
  44. theorem OAI.BorsukNine.FiniteObstruction.c13859 line 389
  45. theorem OAI.BorsukNine.FiniteObstruction.c13982 line 397
  46. theorem OAI.BorsukNine.FiniteObstruction.c13983 line 405
  47. theorem OAI.BorsukNine.FiniteObstruction.c13985 line 413
  48. theorem OAI.BorsukNine.FiniteObstruction.c13987 line 421
  49. theorem OAI.BorsukNine.FiniteObstruction.c13993 line 429