OAI/Geometry/Borsuk/FiniteCases/Cases051.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c17587 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c17594 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c17596 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c17602 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c17603 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c17611 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c17612 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c17619 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c17621 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c17622 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c17624 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c17625 line 117
  13. theorem OAI.BorsukNine.FiniteObstruction.c17626 line 125
  14. theorem OAI.BorsukNine.FiniteObstruction.c17627 line 133
  15. theorem OAI.BorsukNine.FiniteObstruction.c17628 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c17634 line 149
  17. theorem OAI.BorsukNine.FiniteObstruction.c17636 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c17645 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c17651 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c17675 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c17730 line 195
  22. theorem OAI.BorsukNine.FiniteObstruction.c17732 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c17735 line 215
  24. theorem OAI.BorsukNine.FiniteObstruction.c17762 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c17763 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c17768 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c17769 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c17774 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c17777 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c17779 line 273
  31. theorem OAI.BorsukNine.FiniteObstruction.c17781 line 281
  32. theorem OAI.BorsukNine.FiniteObstruction.c17790 line 289
  33. theorem OAI.BorsukNine.FiniteObstruction.c17817 line 299
  34. theorem OAI.BorsukNine.FiniteObstruction.c17824 line 309
  35. theorem OAI.BorsukNine.FiniteObstruction.c17826 line 319
  36. theorem OAI.BorsukNine.FiniteObstruction.c17860 line 329
  37. theorem OAI.BorsukNine.FiniteObstruction.c17879 line 339
  38. theorem OAI.BorsukNine.FiniteObstruction.c17881 line 349
  39. theorem OAI.BorsukNine.FiniteObstruction.c17883 line 359
  40. theorem OAI.BorsukNine.FiniteObstruction.c17885 line 369
  41. theorem OAI.BorsukNine.FiniteObstruction.c17899 line 379
  42. theorem OAI.BorsukNine.FiniteObstruction.c17902 line 389
  43. theorem OAI.BorsukNine.FiniteObstruction.c17908 line 397
  44. theorem OAI.BorsukNine.FiniteObstruction.c17957 line 405
  45. theorem OAI.BorsukNine.FiniteObstruction.c18005 line 415
  46. theorem OAI.BorsukNine.FiniteObstruction.c18007 line 425