OAI/Geometry/Borsuk/FiniteCases/Cases104.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c31601 line 13
  2. theorem OAI.BorsukNine.FiniteObstruction.c31604 line 28
  3. theorem OAI.BorsukNine.FiniteObstruction.c31606 line 43
  4. theorem OAI.BorsukNine.FiniteObstruction.c31607 line 58
  5. theorem OAI.BorsukNine.FiniteObstruction.c31614 line 73
  6. theorem OAI.BorsukNine.FiniteObstruction.c31621 line 88
  7. theorem OAI.BorsukNine.FiniteObstruction.c31622 line 103
  8. theorem OAI.BorsukNine.FiniteObstruction.c31624 line 118
  9. theorem OAI.BorsukNine.FiniteObstruction.c31625 line 133
  10. theorem OAI.BorsukNine.FiniteObstruction.c31627 line 148
  11. theorem OAI.BorsukNine.FiniteObstruction.c31628 line 157
  12. theorem OAI.BorsukNine.FiniteObstruction.c31629 line 166
  13. theorem OAI.BorsukNine.FiniteObstruction.c31630 line 175
  14. theorem OAI.BorsukNine.FiniteObstruction.c31631 line 184
  15. theorem OAI.BorsukNine.FiniteObstruction.c31632 line 193
  16. theorem OAI.BorsukNine.FiniteObstruction.c31633 line 202
  17. theorem OAI.BorsukNine.FiniteObstruction.c31634 line 211
  18. theorem OAI.BorsukNine.FiniteObstruction.c31635 line 220
  19. theorem OAI.BorsukNine.FiniteObstruction.c31636 line 229
  20. theorem OAI.BorsukNine.FiniteObstruction.c31637 line 238
  21. theorem OAI.BorsukNine.FiniteObstruction.c31639 line 247
  22. theorem OAI.BorsukNine.FiniteObstruction.c31640 line 256
  23. theorem OAI.BorsukNine.FiniteObstruction.c31641 line 265
  24. theorem OAI.BorsukNine.FiniteObstruction.c31642 line 274
  25. theorem OAI.BorsukNine.FiniteObstruction.c31643 line 283
  26. theorem OAI.BorsukNine.FiniteObstruction.c31644 line 292
  27. theorem OAI.BorsukNine.FiniteObstruction.c31645 line 301
  28. theorem OAI.BorsukNine.FiniteObstruction.c31646 line 310
  29. theorem OAI.BorsukNine.FiniteObstruction.c31647 line 319
  30. theorem OAI.BorsukNine.FiniteObstruction.c31649 line 328
  31. theorem OAI.BorsukNine.FiniteObstruction.c31651 line 337
  32. theorem OAI.BorsukNine.FiniteObstruction.c31653 line 346
  33. theorem OAI.BorsukNine.FiniteObstruction.c31655 line 355
  34. theorem OAI.BorsukNine.FiniteObstruction.c31657 line 364
  35. theorem OAI.BorsukNine.FiniteObstruction.c31658 line 373
  36. theorem OAI.BorsukNine.FiniteObstruction.c31659 line 382
  37. theorem OAI.BorsukNine.FiniteObstruction.c31660 line 391
  38. theorem OAI.BorsukNine.FiniteObstruction.c31662 line 400
  39. theorem OAI.BorsukNine.FiniteObstruction.c31663 line 409
  40. theorem OAI.BorsukNine.FiniteObstruction.c31665 line 418
  41. theorem OAI.BorsukNine.FiniteObstruction.c31666 line 427