OAI/Geometry/Borsuk/FiniteCases/Cases064.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c24148 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c24151 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c24152 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c24153 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c24154 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c24156 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c24170 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c24172 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c24179 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c24180 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c24182 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c24184 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c24204 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c24210 line 139
  15. theorem OAI.BorsukNine.FiniteObstruction.c24216 line 147
  16. theorem OAI.BorsukNine.FiniteObstruction.c24217 line 155
  17. theorem OAI.BorsukNine.FiniteObstruction.c24219 line 163
  18. theorem OAI.BorsukNine.FiniteObstruction.c24223 line 171
  19. theorem OAI.BorsukNine.FiniteObstruction.c24241 line 181
  20. theorem OAI.BorsukNine.FiniteObstruction.c24265 line 191
  21. theorem OAI.BorsukNine.FiniteObstruction.c24267 line 201
  22. theorem OAI.BorsukNine.FiniteObstruction.c24277 line 211
  23. theorem OAI.BorsukNine.FiniteObstruction.c24285 line 221
  24. theorem OAI.BorsukNine.FiniteObstruction.c24304 line 231
  25. theorem OAI.BorsukNine.FiniteObstruction.c24319 line 241
  26. theorem OAI.BorsukNine.FiniteObstruction.c24343 line 251
  27. theorem OAI.BorsukNine.FiniteObstruction.c24353 line 259
  28. theorem OAI.BorsukNine.FiniteObstruction.c24358 line 267
  29. theorem OAI.BorsukNine.FiniteObstruction.c24359 line 275
  30. theorem OAI.BorsukNine.FiniteObstruction.c24365 line 283
  31. theorem OAI.BorsukNine.FiniteObstruction.c24375 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c24405 line 303
  33. theorem OAI.BorsukNine.FiniteObstruction.c24436 line 313
  34. theorem OAI.BorsukNine.FiniteObstruction.c24459 line 323
  35. theorem OAI.BorsukNine.FiniteObstruction.c24464 line 333
  36. theorem OAI.BorsukNine.FiniteObstruction.c24468 line 343
  37. theorem OAI.BorsukNine.FiniteObstruction.c24515 line 353
  38. theorem OAI.BorsukNine.FiniteObstruction.c24536 line 363
  39. theorem OAI.BorsukNine.FiniteObstruction.c24545 line 373
  40. theorem OAI.BorsukNine.FiniteObstruction.c24547 line 383
  41. theorem OAI.BorsukNine.FiniteObstruction.c24623 line 393
  42. theorem OAI.BorsukNine.FiniteObstruction.c24626 line 401
  43. theorem OAI.BorsukNine.FiniteObstruction.c24632 line 409
  44. theorem OAI.BorsukNine.FiniteObstruction.c24633 line 417
  45. theorem OAI.BorsukNine.FiniteObstruction.c24638 line 425