OAI/Geometry/Borsuk/FiniteCases/Cases047.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c15261 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c15273 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c15336 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c15337 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c15360 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c15364 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c15391 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c15397 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c15437 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c15483 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c15489 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c15497 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c15505 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c15510 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c15519 line 145
  16. theorem OAI.BorsukNine.FiniteObstruction.c15521 line 155
  17. theorem OAI.BorsukNine.FiniteObstruction.c15528 line 165
  18. theorem OAI.BorsukNine.FiniteObstruction.c15529 line 173
  19. theorem OAI.BorsukNine.FiniteObstruction.c15532 line 181
  20. theorem OAI.BorsukNine.FiniteObstruction.c15533 line 189
  21. theorem OAI.BorsukNine.FiniteObstruction.c15537 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c15538 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c15567 line 213
  24. theorem OAI.BorsukNine.FiniteObstruction.c15614 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c15622 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c15623 line 243
  27. theorem OAI.BorsukNine.FiniteObstruction.c15638 line 253
  28. theorem OAI.BorsukNine.FiniteObstruction.c15651 line 263
  29. theorem OAI.BorsukNine.FiniteObstruction.c15662 line 273
  30. theorem OAI.BorsukNine.FiniteObstruction.c15669 line 281
  31. theorem OAI.BorsukNine.FiniteObstruction.c15719 line 289
  32. theorem OAI.BorsukNine.FiniteObstruction.c15738 line 299
  33. theorem OAI.BorsukNine.FiniteObstruction.c15758 line 309
  34. theorem OAI.BorsukNine.FiniteObstruction.c15766 line 319
  35. theorem OAI.BorsukNine.FiniteObstruction.c15781 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c15783 line 339
  37. theorem OAI.BorsukNine.FiniteObstruction.c15811 line 349
  38. theorem OAI.BorsukNine.FiniteObstruction.c15857 line 357
  39. theorem OAI.BorsukNine.FiniteObstruction.c15869 line 367
  40. theorem OAI.BorsukNine.FiniteObstruction.c15888 line 377
  41. theorem OAI.BorsukNine.FiniteObstruction.c15915 line 387
  42. theorem OAI.BorsukNine.FiniteObstruction.c15939 line 397
  43. theorem OAI.BorsukNine.FiniteObstruction.c15945 line 407
  44. theorem OAI.BorsukNine.FiniteObstruction.c15946 line 415
  45. theorem OAI.BorsukNine.FiniteObstruction.c15947 line 423