OAI/Geometry/Borsuk/FiniteCases/Cases026.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c3411 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c3422 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c3483 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c3484 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c3485 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c3488 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c3489 line 63
  8. theorem OAI.BorsukNine.FiniteObstruction.c3490 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c3491 line 79
  10. theorem OAI.BorsukNine.FiniteObstruction.c3492 line 87
  11. theorem OAI.BorsukNine.FiniteObstruction.c3493 line 95
  12. theorem OAI.BorsukNine.FiniteObstruction.c3496 line 103
  13. theorem OAI.BorsukNine.FiniteObstruction.c3497 line 111
  14. theorem OAI.BorsukNine.FiniteObstruction.c3499 line 119
  15. theorem OAI.BorsukNine.FiniteObstruction.c3503 line 127
  16. theorem OAI.BorsukNine.FiniteObstruction.c3511 line 137
  17. theorem OAI.BorsukNine.FiniteObstruction.c3513 line 147
  18. theorem OAI.BorsukNine.FiniteObstruction.c3515 line 157
  19. theorem OAI.BorsukNine.FiniteObstruction.c3567 line 167
  20. theorem OAI.BorsukNine.FiniteObstruction.c3569 line 177
  21. theorem OAI.BorsukNine.FiniteObstruction.c3623 line 187
  22. theorem OAI.BorsukNine.FiniteObstruction.c3735 line 195
  23. theorem OAI.BorsukNine.FiniteObstruction.c3764 line 205
  24. theorem OAI.BorsukNine.FiniteObstruction.c3779 line 213
  25. theorem OAI.BorsukNine.FiniteObstruction.c3817 line 221
  26. theorem OAI.BorsukNine.FiniteObstruction.c3846 line 231
  27. theorem OAI.BorsukNine.FiniteObstruction.c3850 line 241
  28. theorem OAI.BorsukNine.FiniteObstruction.c3865 line 251
  29. theorem OAI.BorsukNine.FiniteObstruction.c3901 line 261
  30. theorem OAI.BorsukNine.FiniteObstruction.c3902 line 271
  31. theorem OAI.BorsukNine.FiniteObstruction.c3904 line 279
  32. theorem OAI.BorsukNine.FiniteObstruction.c3909 line 287
  33. theorem OAI.BorsukNine.FiniteObstruction.c3957 line 295
  34. theorem OAI.BorsukNine.FiniteObstruction.c3984 line 305
  35. theorem OAI.BorsukNine.FiniteObstruction.c3989 line 315
  36. theorem OAI.BorsukNine.FiniteObstruction.c3997 line 325
  37. theorem OAI.BorsukNine.FiniteObstruction.c4004 line 335
  38. theorem OAI.BorsukNine.FiniteObstruction.c4005 line 345
  39. theorem OAI.BorsukNine.FiniteObstruction.c4008 line 355
  40. theorem OAI.BorsukNine.FiniteObstruction.c4024 line 365
  41. theorem OAI.BorsukNine.FiniteObstruction.c4025 line 375
  42. theorem OAI.BorsukNine.FiniteObstruction.c4041 line 385
  43. theorem OAI.BorsukNine.FiniteObstruction.c4045 line 395
  44. theorem OAI.BorsukNine.FiniteObstruction.c4048 line 403
  45. theorem OAI.BorsukNine.FiniteObstruction.c4139 line 411
  46. theorem OAI.BorsukNine.FiniteObstruction.c4141 line 421