OAI/Geometry/Borsuk/FiniteCases/Cases108.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c32212 line 18
  2. theorem OAI.BorsukNine.FiniteObstruction.c32213 line 27
  3. theorem OAI.BorsukNine.FiniteObstruction.c32215 line 36
  4. theorem OAI.BorsukNine.FiniteObstruction.c32216 line 45
  5. theorem OAI.BorsukNine.FiniteObstruction.c32225 line 54
  6. theorem OAI.BorsukNine.FiniteObstruction.c32227 line 63
  7. theorem OAI.BorsukNine.FiniteObstruction.c32229 line 72
  8. theorem OAI.BorsukNine.FiniteObstruction.c32235 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c32243 line 90
  10. theorem OAI.BorsukNine.FiniteObstruction.c32247 line 99
  11. theorem OAI.BorsukNine.FiniteObstruction.c32248 line 108
  12. theorem OAI.BorsukNine.FiniteObstruction.c32250 line 117
  13. theorem OAI.BorsukNine.FiniteObstruction.c32252 line 126
  14. theorem OAI.BorsukNine.FiniteObstruction.c32267 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c32277 line 144
  16. theorem OAI.BorsukNine.FiniteObstruction.c32282 line 153
  17. theorem OAI.BorsukNine.FiniteObstruction.c32283 line 162
  18. theorem OAI.BorsukNine.FiniteObstruction.c32287 line 171
  19. theorem OAI.BorsukNine.FiniteObstruction.c32301 line 180
  20. theorem OAI.BorsukNine.FiniteObstruction.c32303 line 189
  21. theorem OAI.BorsukNine.FiniteObstruction.c32317 line 198
  22. theorem OAI.BorsukNine.FiniteObstruction.c32323 line 207
  23. theorem OAI.BorsukNine.FiniteObstruction.c32324 line 216
  24. theorem OAI.BorsukNine.FiniteObstruction.c32326 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c32337 line 234
  26. theorem OAI.BorsukNine.FiniteObstruction.c32347 line 243
  27. theorem OAI.BorsukNine.FiniteObstruction.c32367 line 252
  28. theorem OAI.BorsukNine.FiniteObstruction.c32374 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c32375 line 270
  30. theorem OAI.BorsukNine.FiniteObstruction.c32382 line 279
  31. theorem OAI.BorsukNine.FiniteObstruction.c32385 line 288
  32. theorem OAI.BorsukNine.FiniteObstruction.c32387 line 297
  33. theorem OAI.BorsukNine.FiniteObstruction.c32395 line 306
  34. theorem OAI.BorsukNine.FiniteObstruction.c32396 line 315
  35. theorem OAI.BorsukNine.FiniteObstruction.c32397 line 324
  36. theorem OAI.BorsukNine.FiniteObstruction.c32398 line 333
  37. theorem OAI.BorsukNine.FiniteObstruction.c32405 line 342
  38. theorem OAI.BorsukNine.FiniteObstruction.c32406 line 351
  39. theorem OAI.BorsukNine.FiniteObstruction.c32407 line 360
  40. theorem OAI.BorsukNine.FiniteObstruction.c32411 line 369
  41. theorem OAI.BorsukNine.FiniteObstruction.c32412 line 378
  42. theorem OAI.BorsukNine.FiniteObstruction.c32415 line 387
  43. theorem OAI.BorsukNine.FiniteObstruction.c32416 line 396
  44. theorem OAI.BorsukNine.FiniteObstruction.c32424 line 405
  45. theorem OAI.BorsukNine.FiniteObstruction.c32425 line 414
  46. theorem OAI.BorsukNine.FiniteObstruction.c32426 line 423
  47. theorem OAI.BorsukNine.FiniteObstruction.c32427 line 432