OAI/Geometry/Borsuk/FiniteCases/Cases030.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c6355 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c6362 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c6363 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c6409 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c6417 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c6423 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c6424 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c6426 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c6427 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c6428 line 93
  11. theorem OAI.BorsukNine.FiniteObstruction.c6430 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c6431 line 109
  13. theorem OAI.BorsukNine.FiniteObstruction.c6434 line 117
  14. theorem OAI.BorsukNine.FiniteObstruction.c6435 line 125
  15. theorem OAI.BorsukNine.FiniteObstruction.c6436 line 133
  16. theorem OAI.BorsukNine.FiniteObstruction.c6438 line 141
  17. theorem OAI.BorsukNine.FiniteObstruction.c6439 line 149
  18. theorem OAI.BorsukNine.FiniteObstruction.c6441 line 157
  19. theorem OAI.BorsukNine.FiniteObstruction.c6443 line 165
  20. theorem OAI.BorsukNine.FiniteObstruction.c6473 line 175
  21. theorem OAI.BorsukNine.FiniteObstruction.c6475 line 185
  22. theorem OAI.BorsukNine.FiniteObstruction.c6490 line 195
  23. theorem OAI.BorsukNine.FiniteObstruction.c6498 line 205
  24. theorem OAI.BorsukNine.FiniteObstruction.c6502 line 215
  25. theorem OAI.BorsukNine.FiniteObstruction.c6531 line 225
  26. theorem OAI.BorsukNine.FiniteObstruction.c6535 line 235
  27. theorem OAI.BorsukNine.FiniteObstruction.c6558 line 245
  28. theorem OAI.BorsukNine.FiniteObstruction.c6563 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c6625 line 263
  30. theorem OAI.BorsukNine.FiniteObstruction.c6654 line 273
  31. theorem OAI.BorsukNine.FiniteObstruction.c6669 line 283
  32. theorem OAI.BorsukNine.FiniteObstruction.c6671 line 293
  33. theorem OAI.BorsukNine.FiniteObstruction.c6685 line 303
  34. theorem OAI.BorsukNine.FiniteObstruction.c6708 line 313
  35. theorem OAI.BorsukNine.FiniteObstruction.c6709 line 321
  36. theorem OAI.BorsukNine.FiniteObstruction.c6721 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c6727 line 337
  38. theorem OAI.BorsukNine.FiniteObstruction.c6757 line 347
  39. theorem OAI.BorsukNine.FiniteObstruction.c6786 line 357
  40. theorem OAI.BorsukNine.FiniteObstruction.c6790 line 367
  41. theorem OAI.BorsukNine.FiniteObstruction.c6802 line 377
  42. theorem OAI.BorsukNine.FiniteObstruction.c6818 line 387
  43. theorem OAI.BorsukNine.FiniteObstruction.c6835 line 397
  44. theorem OAI.BorsukNine.FiniteObstruction.c6843 line 407
  45. theorem OAI.BorsukNine.FiniteObstruction.c6847 line 415
  46. theorem OAI.BorsukNine.FiniteObstruction.c6848 line 423