OAI/Geometry/Borsuk/FiniteCases/Cases024.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c2153 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c2176 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c2207 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c2221 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c2224 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c2232 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c2233 line 67
  8. theorem OAI.BorsukNine.FiniteObstruction.c2235 line 75
  9. theorem OAI.BorsukNine.FiniteObstruction.c2239 line 83
  10. theorem OAI.BorsukNine.FiniteObstruction.c2241 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c2247 line 99
  12. theorem OAI.BorsukNine.FiniteObstruction.c2255 line 109
  13. theorem OAI.BorsukNine.FiniteObstruction.c2270 line 119
  14. theorem OAI.BorsukNine.FiniteObstruction.c2324 line 129
  15. theorem OAI.BorsukNine.FiniteObstruction.c2363 line 139
  16. theorem OAI.BorsukNine.FiniteObstruction.c2365 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c2367 line 155
  18. theorem OAI.BorsukNine.FiniteObstruction.c2368 line 163
  19. theorem OAI.BorsukNine.FiniteObstruction.c2369 line 171
  20. theorem OAI.BorsukNine.FiniteObstruction.c2371 line 179
  21. theorem OAI.BorsukNine.FiniteObstruction.c2372 line 187
  22. theorem OAI.BorsukNine.FiniteObstruction.c2373 line 195
  23. theorem OAI.BorsukNine.FiniteObstruction.c2378 line 203
  24. theorem OAI.BorsukNine.FiniteObstruction.c2441 line 211
  25. theorem OAI.BorsukNine.FiniteObstruction.c2449 line 221
  26. theorem OAI.BorsukNine.FiniteObstruction.c2463 line 231
  27. theorem OAI.BorsukNine.FiniteObstruction.c2505 line 241
  28. theorem OAI.BorsukNine.FiniteObstruction.c2506 line 249
  29. theorem OAI.BorsukNine.FiniteObstruction.c2509 line 257
  30. theorem OAI.BorsukNine.FiniteObstruction.c2515 line 265
  31. theorem OAI.BorsukNine.FiniteObstruction.c2517 line 273
  32. theorem OAI.BorsukNine.FiniteObstruction.c2525 line 281
  33. theorem OAI.BorsukNine.FiniteObstruction.c2533 line 291
  34. theorem OAI.BorsukNine.FiniteObstruction.c2543 line 301
  35. theorem OAI.BorsukNine.FiniteObstruction.c2555 line 311
  36. theorem OAI.BorsukNine.FiniteObstruction.c2563 line 321
  37. theorem OAI.BorsukNine.FiniteObstruction.c2583 line 331
  38. theorem OAI.BorsukNine.FiniteObstruction.c2620 line 341
  39. theorem OAI.BorsukNine.FiniteObstruction.c2623 line 351
  40. theorem OAI.BorsukNine.FiniteObstruction.c2643 line 361
  41. theorem OAI.BorsukNine.FiniteObstruction.c2644 line 369
  42. theorem OAI.BorsukNine.FiniteObstruction.c2645 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c2646 line 385
  44. theorem OAI.BorsukNine.FiniteObstruction.c2647 line 393
  45. theorem OAI.BorsukNine.FiniteObstruction.c2653 line 401
  46. theorem OAI.BorsukNine.FiniteObstruction.c2654 line 409
  47. theorem OAI.BorsukNine.FiniteObstruction.c2655 line 417
  48. theorem OAI.BorsukNine.FiniteObstruction.c2656 line 425