OAI/Geometry/Borsuk/FiniteCases/Cases017.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BorsukNine.FiniteObstruction.c1491 line 11
2. theorem OAI.BorsukNine.FiniteObstruction.c1494 line 28
3. theorem OAI.BorsukNine.FiniteObstruction.c1495 line 33
4. theorem OAI.BorsukNine.FiniteObstruction.c1496 line 50
5. theorem OAI.BorsukNine.FiniteObstruction.c1497 line 55
6. theorem OAI.BorsukNine.FiniteObstruction.c1499 line 72
7. theorem OAI.BorsukNine.FiniteObstruction.c1500 line 89
8. theorem OAI.BorsukNine.FiniteObstruction.c1501 line 94
9. theorem OAI.BorsukNine.FiniteObstruction.c1502 line 111
10. theorem OAI.BorsukNine.FiniteObstruction.c1504 line 128
11. theorem OAI.BorsukNine.FiniteObstruction.c1506 line 145
12. theorem OAI.BorsukNine.FiniteObstruction.c1508 line 162
13. theorem OAI.BorsukNine.FiniteObstruction.c1510 line 179
14. theorem OAI.BorsukNine.FiniteObstruction.c1517 line 196
15. theorem OAI.BorsukNine.FiniteObstruction.c1518 line 213
16. theorem OAI.BorsukNine.FiniteObstruction.c1521 line 218
17. theorem OAI.BorsukNine.FiniteObstruction.c1522 line 235
18. theorem OAI.BorsukNine.FiniteObstruction.c1524 line 240
19. theorem OAI.BorsukNine.FiniteObstruction.c1525 line 245
20. theorem OAI.BorsukNine.FiniteObstruction.c1532 line 262
21. theorem OAI.BorsukNine.FiniteObstruction.c1533 line 279
22. theorem OAI.BorsukNine.FiniteObstruction.c1534 line 284
23. theorem OAI.BorsukNine.FiniteObstruction.c1535 line 301
24. theorem OAI.BorsukNine.FiniteObstruction.c1536 line 306
25. theorem OAI.BorsukNine.FiniteObstruction.c1538 line 323
26. theorem OAI.BorsukNine.FiniteObstruction.c1539 line 340
27. theorem OAI.BorsukNine.FiniteObstruction.c1540 line 345
28. theorem OAI.BorsukNine.FiniteObstruction.c1547 line 362
29. theorem OAI.BorsukNine.FiniteObstruction.c1549 line 379
30. theorem OAI.BorsukNine.FiniteObstruction.c1562 line 396
31. theorem OAI.BorsukNine.FiniteObstruction.c1563 line 413
32. theorem OAI.BorsukNine.FiniteObstruction.c1564 line 418