OAI/Geometry/Borsuk/FiniteCases/Cases039.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c11347 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c11353 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c11355 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c11374 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c11376 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c11379 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c11385 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c11387 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c11414 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c11430 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c11432 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c11439 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c11442 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c11463 line 141
  15. theorem OAI.BorsukNine.FiniteObstruction.c11465 line 149
  16. theorem OAI.BorsukNine.FiniteObstruction.c11478 line 157
  17. theorem OAI.BorsukNine.FiniteObstruction.c11483 line 165
  18. theorem OAI.BorsukNine.FiniteObstruction.c11485 line 175
  19. theorem OAI.BorsukNine.FiniteObstruction.c11487 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c11493 line 195
  21. theorem OAI.BorsukNine.FiniteObstruction.c11495 line 205
  22. theorem OAI.BorsukNine.FiniteObstruction.c11505 line 215
  23. theorem OAI.BorsukNine.FiniteObstruction.c11513 line 225
  24. theorem OAI.BorsukNine.FiniteObstruction.c11515 line 235
  25. theorem OAI.BorsukNine.FiniteObstruction.c11547 line 245
  26. theorem OAI.BorsukNine.FiniteObstruction.c11551 line 255
  27. theorem OAI.BorsukNine.FiniteObstruction.c11572 line 265
  28. theorem OAI.BorsukNine.FiniteObstruction.c11606 line 275
  29. theorem OAI.BorsukNine.FiniteObstruction.c11613 line 283
  30. theorem OAI.BorsukNine.FiniteObstruction.c11618 line 291
  31. theorem OAI.BorsukNine.FiniteObstruction.c11619 line 299
  32. theorem OAI.BorsukNine.FiniteObstruction.c11696 line 307
  33. theorem OAI.BorsukNine.FiniteObstruction.c11722 line 317
  34. theorem OAI.BorsukNine.FiniteObstruction.c11727 line 327
  35. theorem OAI.BorsukNine.FiniteObstruction.c11743 line 337
  36. theorem OAI.BorsukNine.FiniteObstruction.c11751 line 345
  37. theorem OAI.BorsukNine.FiniteObstruction.c11754 line 353
  38. theorem OAI.BorsukNine.FiniteObstruction.c11755 line 361
  39. theorem OAI.BorsukNine.FiniteObstruction.c11767 line 369
  40. theorem OAI.BorsukNine.FiniteObstruction.c11773 line 379
  41. theorem OAI.BorsukNine.FiniteObstruction.c11775 line 389
  42. theorem OAI.BorsukNine.FiniteObstruction.c11807 line 399
  43. theorem OAI.BorsukNine.FiniteObstruction.c11851 line 409
  44. theorem OAI.BorsukNine.FiniteObstruction.c11852 line 419
  45. theorem OAI.BorsukNine.FiniteObstruction.c11859 line 429