OAI/Geometry/Borsuk/FiniteCases/Cases022.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1858 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1860 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c1861 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c1865 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c1866 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c1867 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c1868 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c1869 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c1870 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c1872 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c1878 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c1879 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c1880 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c1881 line 141
  15. theorem OAI.BorsukNine.FiniteObstruction.c1882 line 151
  16. theorem OAI.BorsukNine.FiniteObstruction.c1883 line 161
  17. theorem OAI.BorsukNine.FiniteObstruction.c1884 line 171
  18. theorem OAI.BorsukNine.FiniteObstruction.c1885 line 181
  19. theorem OAI.BorsukNine.FiniteObstruction.c1886 line 191
  20. theorem OAI.BorsukNine.FiniteObstruction.c1887 line 201
  21. theorem OAI.BorsukNine.FiniteObstruction.c1889 line 211
  22. theorem OAI.BorsukNine.FiniteObstruction.c1890 line 221
  23. theorem OAI.BorsukNine.FiniteObstruction.c1893 line 231
  24. theorem OAI.BorsukNine.FiniteObstruction.c1894 line 241
  25. theorem OAI.BorsukNine.FiniteObstruction.c1895 line 251
  26. theorem OAI.BorsukNine.FiniteObstruction.c1896 line 261
  27. theorem OAI.BorsukNine.FiniteObstruction.c1897 line 271
  28. theorem OAI.BorsukNine.FiniteObstruction.c1898 line 281
  29. theorem OAI.BorsukNine.FiniteObstruction.c1899 line 291
  30. theorem OAI.BorsukNine.FiniteObstruction.c1900 line 301
  31. theorem OAI.BorsukNine.FiniteObstruction.c1901 line 311
  32. theorem OAI.BorsukNine.FiniteObstruction.c1902 line 321
  33. theorem OAI.BorsukNine.FiniteObstruction.c1903 line 331
  34. theorem OAI.BorsukNine.FiniteObstruction.c1904 line 341
  35. theorem OAI.BorsukNine.FiniteObstruction.c1906 line 351
  36. theorem OAI.BorsukNine.FiniteObstruction.c1907 line 361
  37. theorem OAI.BorsukNine.FiniteObstruction.c1908 line 371
  38. theorem OAI.BorsukNine.FiniteObstruction.c1910 line 381
  39. theorem OAI.BorsukNine.FiniteObstruction.c1911 line 391
  40. theorem OAI.BorsukNine.FiniteObstruction.c1912 line 401
  41. theorem OAI.BorsukNine.FiniteObstruction.c1913 line 411
  42. theorem OAI.BorsukNine.FiniteObstruction.c1914 line 421