OAI/Geometry/Borsuk/FiniteCases/Cases004.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c312 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c313 line 28
  3. theorem OAI.BorsukNine.FiniteObstruction.c314 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c317 line 50
  5. theorem OAI.BorsukNine.FiniteObstruction.c318 line 67
  6. theorem OAI.BorsukNine.FiniteObstruction.c322 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c324 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c326 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c327 line 87
  10. theorem OAI.BorsukNine.FiniteObstruction.c328 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c329 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c332 line 126
  13. theorem OAI.BorsukNine.FiniteObstruction.c334 line 143
  14. theorem OAI.BorsukNine.FiniteObstruction.c336 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c338 line 177
  16. theorem OAI.BorsukNine.FiniteObstruction.c339 line 194
  17. theorem OAI.BorsukNine.FiniteObstruction.c340 line 199
  18. theorem OAI.BorsukNine.FiniteObstruction.c341 line 216
  19. theorem OAI.BorsukNine.FiniteObstruction.c344 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c347 line 238
  21. theorem OAI.BorsukNine.FiniteObstruction.c348 line 255
  22. theorem OAI.BorsukNine.FiniteObstruction.c350 line 260
  23. theorem OAI.BorsukNine.FiniteObstruction.c352 line 265
  24. theorem OAI.BorsukNine.FiniteObstruction.c356 line 270
  25. theorem OAI.BorsukNine.FiniteObstruction.c357 line 275
  26. theorem OAI.BorsukNine.FiniteObstruction.c359 line 292
  27. theorem OAI.BorsukNine.FiniteObstruction.c360 line 309
  28. theorem OAI.BorsukNine.FiniteObstruction.c361 line 314
  29. theorem OAI.BorsukNine.FiniteObstruction.c362 line 331
  30. theorem OAI.BorsukNine.FiniteObstruction.c369 line 348
  31. theorem OAI.BorsukNine.FiniteObstruction.c370 line 353
  32. theorem OAI.BorsukNine.FiniteObstruction.c372 line 370
  33. theorem OAI.BorsukNine.FiniteObstruction.c374 line 387
  34. theorem OAI.BorsukNine.FiniteObstruction.c376 line 404
  35. theorem OAI.BorsukNine.FiniteObstruction.c380 line 421
  36. theorem OAI.BorsukNine.FiniteObstruction.c382 line 426