OAI/Geometry/Borsuk/FiniteCases/Cases002.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c155 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c157 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c160 line 21
  4. theorem OAI.BorsukNine.FiniteObstruction.c163 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c165 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c166 line 48
  7. theorem OAI.BorsukNine.FiniteObstruction.c170 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c171 line 70
  9. theorem OAI.BorsukNine.FiniteObstruction.c172 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c174 line 92
  11. theorem OAI.BorsukNine.FiniteObstruction.c176 line 97
  12. theorem OAI.BorsukNine.FiniteObstruction.c178 line 102
  13. theorem OAI.BorsukNine.FiniteObstruction.c180 line 107
  14. theorem OAI.BorsukNine.FiniteObstruction.c182 line 112
  15. theorem OAI.BorsukNine.FiniteObstruction.c184 line 129
  16. theorem OAI.BorsukNine.FiniteObstruction.c185 line 146
  17. theorem OAI.BorsukNine.FiniteObstruction.c187 line 151
  18. theorem OAI.BorsukNine.FiniteObstruction.c188 line 156
  19. theorem OAI.BorsukNine.FiniteObstruction.c189 line 173
  20. theorem OAI.BorsukNine.FiniteObstruction.c190 line 178
  21. theorem OAI.BorsukNine.FiniteObstruction.c192 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c193 line 212
  23. theorem OAI.BorsukNine.FiniteObstruction.c197 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c199 line 234
  25. theorem OAI.BorsukNine.FiniteObstruction.c200 line 251
  26. theorem OAI.BorsukNine.FiniteObstruction.c202 line 256
  27. theorem OAI.BorsukNine.FiniteObstruction.c203 line 261
  28. theorem OAI.BorsukNine.FiniteObstruction.c204 line 278
  29. theorem OAI.BorsukNine.FiniteObstruction.c205 line 283
  30. theorem OAI.BorsukNine.FiniteObstruction.c207 line 300
  31. theorem OAI.BorsukNine.FiniteObstruction.c208 line 317
  32. theorem OAI.BorsukNine.FiniteObstruction.c209 line 322
  33. theorem OAI.BorsukNine.FiniteObstruction.c210 line 339
  34. theorem OAI.BorsukNine.FiniteObstruction.c211 line 344
  35. theorem OAI.BorsukNine.FiniteObstruction.c212 line 361
  36. theorem OAI.BorsukNine.FiniteObstruction.c213 line 378
  37. theorem OAI.BorsukNine.FiniteObstruction.c214 line 383
  38. theorem OAI.BorsukNine.FiniteObstruction.c215 line 400
  39. theorem OAI.BorsukNine.FiniteObstruction.c216 line 405
  40. theorem OAI.BorsukNine.FiniteObstruction.c217 line 422
  41. theorem OAI.BorsukNine.FiniteObstruction.c224 line 427