OAI/Geometry/Borsuk/FiniteCases/Cases060.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c22090 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c22103 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c22104 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c22105 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c22111 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c22193 line 53
  7. theorem OAI.BorsukNine.FiniteObstruction.c22196 line 63
  8. theorem OAI.BorsukNine.FiniteObstruction.c22197 line 73
  9. theorem OAI.BorsukNine.FiniteObstruction.c22198 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c22199 line 93
  11. theorem OAI.BorsukNine.FiniteObstruction.c22215 line 103
  12. theorem OAI.BorsukNine.FiniteObstruction.c22231 line 113
  13. theorem OAI.BorsukNine.FiniteObstruction.c22242 line 123
  14. theorem OAI.BorsukNine.FiniteObstruction.c22244 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c22357 line 139
  16. theorem OAI.BorsukNine.FiniteObstruction.c22382 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c22383 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c22384 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c22386 line 173
  20. theorem OAI.BorsukNine.FiniteObstruction.c22388 line 181
  21. theorem OAI.BorsukNine.FiniteObstruction.c22389 line 189
  22. theorem OAI.BorsukNine.FiniteObstruction.c22393 line 197
  23. theorem OAI.BorsukNine.FiniteObstruction.c22402 line 205
  24. theorem OAI.BorsukNine.FiniteObstruction.c22423 line 215
  25. theorem OAI.BorsukNine.FiniteObstruction.c22451 line 225
  26. theorem OAI.BorsukNine.FiniteObstruction.c22475 line 235
  27. theorem OAI.BorsukNine.FiniteObstruction.c22477 line 245
  28. theorem OAI.BorsukNine.FiniteObstruction.c22478 line 255
  29. theorem OAI.BorsukNine.FiniteObstruction.c22479 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c22481 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c22483 line 285
  32. theorem OAI.BorsukNine.FiniteObstruction.c22485 line 295
  33. theorem OAI.BorsukNine.FiniteObstruction.c22486 line 305
  34. theorem OAI.BorsukNine.FiniteObstruction.c22487 line 315
  35. theorem OAI.BorsukNine.FiniteObstruction.c22494 line 325
  36. theorem OAI.BorsukNine.FiniteObstruction.c22497 line 335
  37. theorem OAI.BorsukNine.FiniteObstruction.c22502 line 345
  38. theorem OAI.BorsukNine.FiniteObstruction.c22503 line 355
  39. theorem OAI.BorsukNine.FiniteObstruction.c22505 line 365
  40. theorem OAI.BorsukNine.FiniteObstruction.c22506 line 375
  41. theorem OAI.BorsukNine.FiniteObstruction.c22510 line 385
  42. theorem OAI.BorsukNine.FiniteObstruction.c22511 line 395
  43. theorem OAI.BorsukNine.FiniteObstruction.c22512 line 405
  44. theorem OAI.BorsukNine.FiniteObstruction.c22521 line 415
  45. theorem OAI.BorsukNine.FiniteObstruction.c22522 line 425