OAI/Geometry/Borsuk/FiniteCases/Cases049.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c16605 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c16607 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c16611 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c16639 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c16645 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c16649 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c16651 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c16745 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c16746 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c16749 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c16755 line 105
  12. theorem OAI.BorsukNine.FiniteObstruction.c16779 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c16782 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c16784 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c16788 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c16789 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c16797 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c16837 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c16883 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c16885 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c16886 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c16887 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c16889 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c16901 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c16921 line 235
  26. theorem OAI.BorsukNine.FiniteObstruction.c16923 line 245
  27. theorem OAI.BorsukNine.FiniteObstruction.c16924 line 253
  28. theorem OAI.BorsukNine.FiniteObstruction.c16926 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c17049 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c17062 line 279
  31. theorem OAI.BorsukNine.FiniteObstruction.c17063 line 287
  32. theorem OAI.BorsukNine.FiniteObstruction.c17064 line 295
  33. theorem OAI.BorsukNine.FiniteObstruction.c17065 line 303
  34. theorem OAI.BorsukNine.FiniteObstruction.c17066 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c17067 line 319
  36. theorem OAI.BorsukNine.FiniteObstruction.c17068 line 327
  37. theorem OAI.BorsukNine.FiniteObstruction.c17074 line 335
  38. theorem OAI.BorsukNine.FiniteObstruction.c17075 line 343
  39. theorem OAI.BorsukNine.FiniteObstruction.c17082 line 351
  40. theorem OAI.BorsukNine.FiniteObstruction.c17083 line 361
  41. theorem OAI.BorsukNine.FiniteObstruction.c17084 line 371
  42. theorem OAI.BorsukNine.FiniteObstruction.c17085 line 381
  43. theorem OAI.BorsukNine.FiniteObstruction.c17088 line 391
  44. theorem OAI.BorsukNine.FiniteObstruction.c17089 line 401
  45. theorem OAI.BorsukNine.FiniteObstruction.c17130 line 411
  46. theorem OAI.BorsukNine.FiniteObstruction.c17134 line 421