OAI/Geometry/Borsuk/FiniteCases/Cases048.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c15953 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c15959 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c15986 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c15988 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c16009 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c16026 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c16047 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c16071 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c16084 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c16097 line 95
  11. theorem OAI.BorsukNine.FiniteObstruction.c16149 line 103
  12. theorem OAI.BorsukNine.FiniteObstruction.c16184 line 113
  13. theorem OAI.BorsukNine.FiniteObstruction.c16185 line 123
  14. theorem OAI.BorsukNine.FiniteObstruction.c16218 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c16222 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c16225 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c16226 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c16229 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c16233 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c16239 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c16281 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c16289 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c16322 line 211
  24. theorem OAI.BorsukNine.FiniteObstruction.c16324 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c16327 line 231
  26. theorem OAI.BorsukNine.FiniteObstruction.c16349 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c16351 line 251
  28. theorem OAI.BorsukNine.FiniteObstruction.c16365 line 261
  29. theorem OAI.BorsukNine.FiniteObstruction.c16368 line 269
  30. theorem OAI.BorsukNine.FiniteObstruction.c16369 line 277
  31. theorem OAI.BorsukNine.FiniteObstruction.c16374 line 285
  32. theorem OAI.BorsukNine.FiniteObstruction.c16375 line 293
  33. theorem OAI.BorsukNine.FiniteObstruction.c16376 line 301
  34. theorem OAI.BorsukNine.FiniteObstruction.c16384 line 309
  35. theorem OAI.BorsukNine.FiniteObstruction.c16388 line 319
  36. theorem OAI.BorsukNine.FiniteObstruction.c16417 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c16464 line 339
  38. theorem OAI.BorsukNine.FiniteObstruction.c16465 line 349
  39. theorem OAI.BorsukNine.FiniteObstruction.c16467 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c16472 line 369
  41. theorem OAI.BorsukNine.FiniteObstruction.c16473 line 379
  42. theorem OAI.BorsukNine.FiniteObstruction.c16483 line 389
  43. theorem OAI.BorsukNine.FiniteObstruction.c16494 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c16501 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c16504 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c16530 line 427