OAI/Geometry/Borsuk/FiniteCases/Cases063.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c23516 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c23521 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c23531 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c23555 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c23556 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c23565 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c23567 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c23596 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c23620 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c23622 line 97
  11. theorem OAI.BorsukNine.FiniteObstruction.c23650 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c23673 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c23694 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c23705 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c23707 line 145
  16. theorem OAI.BorsukNine.FiniteObstruction.c23796 line 155
  17. theorem OAI.BorsukNine.FiniteObstruction.c23813 line 163
  18. theorem OAI.BorsukNine.FiniteObstruction.c23815 line 173
  19. theorem OAI.BorsukNine.FiniteObstruction.c23820 line 183
  20. theorem OAI.BorsukNine.FiniteObstruction.c23845 line 193
  21. theorem OAI.BorsukNine.FiniteObstruction.c23847 line 203
  22. theorem OAI.BorsukNine.FiniteObstruction.c23923 line 213
  23. theorem OAI.BorsukNine.FiniteObstruction.c23955 line 221
  24. theorem OAI.BorsukNine.FiniteObstruction.c23983 line 231
  25. theorem OAI.BorsukNine.FiniteObstruction.c24039 line 241
  26. theorem OAI.BorsukNine.FiniteObstruction.c24063 line 251
  27. theorem OAI.BorsukNine.FiniteObstruction.c24064 line 259
  28. theorem OAI.BorsukNine.FiniteObstruction.c24068 line 267
  29. theorem OAI.BorsukNine.FiniteObstruction.c24069 line 275
  30. theorem OAI.BorsukNine.FiniteObstruction.c24070 line 283
  31. theorem OAI.BorsukNine.FiniteObstruction.c24071 line 291
  32. theorem OAI.BorsukNine.FiniteObstruction.c24072 line 299
  33. theorem OAI.BorsukNine.FiniteObstruction.c24073 line 307
  34. theorem OAI.BorsukNine.FiniteObstruction.c24074 line 315
  35. theorem OAI.BorsukNine.FiniteObstruction.c24075 line 323
  36. theorem OAI.BorsukNine.FiniteObstruction.c24076 line 331
  37. theorem OAI.BorsukNine.FiniteObstruction.c24085 line 339
  38. theorem OAI.BorsukNine.FiniteObstruction.c24087 line 349
  39. theorem OAI.BorsukNine.FiniteObstruction.c24091 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c24093 line 369
  41. theorem OAI.BorsukNine.FiniteObstruction.c24095 line 379
  42. theorem OAI.BorsukNine.FiniteObstruction.c24096 line 389
  43. theorem OAI.BorsukNine.FiniteObstruction.c24125 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c24127 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c24135 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c24146 line 429