OAI/Geometry/Borsuk/FiniteCases/Cases023.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1915 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1916 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c1917 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c1919 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c1920 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c1922 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c1923 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c1924 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c1925 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c1926 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c1927 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c1930 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c1931 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c1932 line 141
  15. theorem OAI.BorsukNine.FiniteObstruction.c1934 line 151
  16. theorem OAI.BorsukNine.FiniteObstruction.c1935 line 161
  17. theorem OAI.BorsukNine.FiniteObstruction.c1937 line 171
  18. theorem OAI.BorsukNine.FiniteObstruction.c1938 line 181
  19. theorem OAI.BorsukNine.FiniteObstruction.c1939 line 191
  20. theorem OAI.BorsukNine.FiniteObstruction.c1940 line 201
  21. theorem OAI.BorsukNine.FiniteObstruction.c1941 line 211
  22. theorem OAI.BorsukNine.FiniteObstruction.c1943 line 221
  23. theorem OAI.BorsukNine.FiniteObstruction.c1946 line 229
  24. theorem OAI.BorsukNine.FiniteObstruction.c1947 line 237
  25. theorem OAI.BorsukNine.FiniteObstruction.c1949 line 245
  26. theorem OAI.BorsukNine.FiniteObstruction.c1950 line 253
  27. theorem OAI.BorsukNine.FiniteObstruction.c1951 line 261
  28. theorem OAI.BorsukNine.FiniteObstruction.c1953 line 269
  29. theorem OAI.BorsukNine.FiniteObstruction.c1955 line 277
  30. theorem OAI.BorsukNine.FiniteObstruction.c1967 line 285
  31. theorem OAI.BorsukNine.FiniteObstruction.c1971 line 295
  32. theorem OAI.BorsukNine.FiniteObstruction.c1981 line 305
  33. theorem OAI.BorsukNine.FiniteObstruction.c2001 line 315
  34. theorem OAI.BorsukNine.FiniteObstruction.c2002 line 325
  35. theorem OAI.BorsukNine.FiniteObstruction.c2020 line 335
  36. theorem OAI.BorsukNine.FiniteObstruction.c2034 line 345
  37. theorem OAI.BorsukNine.FiniteObstruction.c2084 line 355
  38. theorem OAI.BorsukNine.FiniteObstruction.c2085 line 363
  39. theorem OAI.BorsukNine.FiniteObstruction.c2087 line 371
  40. theorem OAI.BorsukNine.FiniteObstruction.c2089 line 379
  41. theorem OAI.BorsukNine.FiniteObstruction.c2098 line 387
  42. theorem OAI.BorsukNine.FiniteObstruction.c2107 line 395
  43. theorem OAI.BorsukNine.FiniteObstruction.c2113 line 405
  44. theorem OAI.BorsukNine.FiniteObstruction.c2122 line 415
  45. theorem OAI.BorsukNine.FiniteObstruction.c2137 line 425