OAI/Geometry/Borsuk/FiniteCases/Cases043.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c12895 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c12906 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c12911 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c12914 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c12921 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c12927 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c12932 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c12938 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c12939 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c12948 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c12964 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c12971 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c12972 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c12975 line 141
  15. theorem OAI.BorsukNine.FiniteObstruction.c12977 line 151
  16. theorem OAI.BorsukNine.FiniteObstruction.c12982 line 161
  17. theorem OAI.BorsukNine.FiniteObstruction.c12984 line 171
  18. theorem OAI.BorsukNine.FiniteObstruction.c12990 line 181
  19. theorem OAI.BorsukNine.FiniteObstruction.c12992 line 191
  20. theorem OAI.BorsukNine.FiniteObstruction.c12998 line 201
  21. theorem OAI.BorsukNine.FiniteObstruction.c13000 line 211
  22. theorem OAI.BorsukNine.FiniteObstruction.c13015 line 221
  23. theorem OAI.BorsukNine.FiniteObstruction.c13025 line 229
  24. theorem OAI.BorsukNine.FiniteObstruction.c13027 line 239
  25. theorem OAI.BorsukNine.FiniteObstruction.c13033 line 249
  26. theorem OAI.BorsukNine.FiniteObstruction.c13057 line 259
  27. theorem OAI.BorsukNine.FiniteObstruction.c13071 line 269
  28. theorem OAI.BorsukNine.FiniteObstruction.c13089 line 279
  29. theorem OAI.BorsukNine.FiniteObstruction.c13096 line 289
  30. theorem OAI.BorsukNine.FiniteObstruction.c13144 line 299
  31. theorem OAI.BorsukNine.FiniteObstruction.c13145 line 307
  32. theorem OAI.BorsukNine.FiniteObstruction.c13155 line 315
  33. theorem OAI.BorsukNine.FiniteObstruction.c13160 line 323
  34. theorem OAI.BorsukNine.FiniteObstruction.c13275 line 331
  35. theorem OAI.BorsukNine.FiniteObstruction.c13280 line 341
  36. theorem OAI.BorsukNine.FiniteObstruction.c13283 line 351
  37. theorem OAI.BorsukNine.FiniteObstruction.c13284 line 359
  38. theorem OAI.BorsukNine.FiniteObstruction.c13286 line 367
  39. theorem OAI.BorsukNine.FiniteObstruction.c13298 line 375
  40. theorem OAI.BorsukNine.FiniteObstruction.c13307 line 383
  41. theorem OAI.BorsukNine.FiniteObstruction.c13315 line 393
  42. theorem OAI.BorsukNine.FiniteObstruction.c13316 line 403
  43. theorem OAI.BorsukNine.FiniteObstruction.c13351 line 413
  44. theorem OAI.BorsukNine.FiniteObstruction.c13379 line 423