OAI/Geometry/Borsuk/FiniteCases/Cases016.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1427 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1428 line 28
  3. theorem OAI.BorsukNine.FiniteObstruction.c1434 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c1435 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c1437 line 55
  6. theorem OAI.BorsukNine.FiniteObstruction.c1438 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c1439 line 77
  8. theorem OAI.BorsukNine.FiniteObstruction.c1440 line 94
  9. theorem OAI.BorsukNine.FiniteObstruction.c1441 line 99
  10. theorem OAI.BorsukNine.FiniteObstruction.c1442 line 116
  11. theorem OAI.BorsukNine.FiniteObstruction.c1444 line 133
  12. theorem OAI.BorsukNine.FiniteObstruction.c1445 line 150
  13. theorem OAI.BorsukNine.FiniteObstruction.c1449 line 155
  14. theorem OAI.BorsukNine.FiniteObstruction.c1450 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c1452 line 177
  16. theorem OAI.BorsukNine.FiniteObstruction.c1453 line 194
  17. theorem OAI.BorsukNine.FiniteObstruction.c1454 line 199
  18. theorem OAI.BorsukNine.FiniteObstruction.c1456 line 216
  19. theorem OAI.BorsukNine.FiniteObstruction.c1457 line 233
  20. theorem OAI.BorsukNine.FiniteObstruction.c1467 line 250
  21. theorem OAI.BorsukNine.FiniteObstruction.c1468 line 267
  22. theorem OAI.BorsukNine.FiniteObstruction.c1469 line 272
  23. theorem OAI.BorsukNine.FiniteObstruction.c1472 line 289
  24. theorem OAI.BorsukNine.FiniteObstruction.c1475 line 306
  25. theorem OAI.BorsukNine.FiniteObstruction.c1478 line 311
  26. theorem OAI.BorsukNine.FiniteObstruction.c1479 line 328
  27. theorem OAI.BorsukNine.FiniteObstruction.c1480 line 333
  28. theorem OAI.BorsukNine.FiniteObstruction.c1481 line 350
  29. theorem OAI.BorsukNine.FiniteObstruction.c1482 line 355
  30. theorem OAI.BorsukNine.FiniteObstruction.c1484 line 372
  31. theorem OAI.BorsukNine.FiniteObstruction.c1485 line 389
  32. theorem OAI.BorsukNine.FiniteObstruction.c1486 line 394
  33. theorem OAI.BorsukNine.FiniteObstruction.c1487 line 411
  34. theorem OAI.BorsukNine.FiniteObstruction.c1490 line 428