OAI/Geometry/Borsuk/FiniteCases/Cases005.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BorsukNine.FiniteObstruction.c388 line 11
2. theorem OAI.BorsukNine.FiniteObstruction.c392 line 16
3. theorem OAI.BorsukNine.FiniteObstruction.c402 line 33
4. theorem OAI.BorsukNine.FiniteObstruction.c403 line 50
5. theorem OAI.BorsukNine.FiniteObstruction.c407 line 55
6. theorem OAI.BorsukNine.FiniteObstruction.c415 line 72
7. theorem OAI.BorsukNine.FiniteObstruction.c417 line 89
8. theorem OAI.BorsukNine.FiniteObstruction.c421 line 106
9. theorem OAI.BorsukNine.FiniteObstruction.c422 line 123
10. theorem OAI.BorsukNine.FiniteObstruction.c424 line 140
11. theorem OAI.BorsukNine.FiniteObstruction.c426 line 157
12. theorem OAI.BorsukNine.FiniteObstruction.c427 line 174
13. theorem OAI.BorsukNine.FiniteObstruction.c428 line 179
14. theorem OAI.BorsukNine.FiniteObstruction.c429 line 196
15. theorem OAI.BorsukNine.FiniteObstruction.c430 line 201
16. theorem OAI.BorsukNine.FiniteObstruction.c431 line 218
17. theorem OAI.BorsukNine.FiniteObstruction.c432 line 223
18. theorem OAI.BorsukNine.FiniteObstruction.c434 line 240
19. theorem OAI.BorsukNine.FiniteObstruction.c435 line 257
20. theorem OAI.BorsukNine.FiniteObstruction.c436 line 262
21. theorem OAI.BorsukNine.FiniteObstruction.c445 line 279
22. theorem OAI.BorsukNine.FiniteObstruction.c448 line 296
23. theorem OAI.BorsukNine.FiniteObstruction.c450 line 301
24. theorem OAI.BorsukNine.FiniteObstruction.c451 line 306
25. theorem OAI.BorsukNine.FiniteObstruction.c452 line 323
26. theorem OAI.BorsukNine.FiniteObstruction.c454 line 340
27. theorem OAI.BorsukNine.FiniteObstruction.c456 line 357
28. theorem OAI.BorsukNine.FiniteObstruction.c457 line 374
29. theorem OAI.BorsukNine.FiniteObstruction.c459 line 379
30. theorem OAI.BorsukNine.FiniteObstruction.c460 line 384
31. theorem OAI.BorsukNine.FiniteObstruction.c467 line 401
32. theorem OAI.BorsukNine.FiniteObstruction.c469 line 418