OAI/Geometry/Borsuk/FiniteCases/Cases021.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1810 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1811 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c1812 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c1813 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c1814 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c1815 line 51
  7. theorem OAI.BorsukNine.FiniteObstruction.c1816 line 59
  8. theorem OAI.BorsukNine.FiniteObstruction.c1817 line 67
  9. theorem OAI.BorsukNine.FiniteObstruction.c1818 line 75
  10. theorem OAI.BorsukNine.FiniteObstruction.c1819 line 83
  11. theorem OAI.BorsukNine.FiniteObstruction.c1820 line 91
  12. theorem OAI.BorsukNine.FiniteObstruction.c1821 line 99
  13. theorem OAI.BorsukNine.FiniteObstruction.c1822 line 107
  14. theorem OAI.BorsukNine.FiniteObstruction.c1823 line 117
  15. theorem OAI.BorsukNine.FiniteObstruction.c1824 line 127
  16. theorem OAI.BorsukNine.FiniteObstruction.c1825 line 137
  17. theorem OAI.BorsukNine.FiniteObstruction.c1826 line 147
  18. theorem OAI.BorsukNine.FiniteObstruction.c1828 line 157
  19. theorem OAI.BorsukNine.FiniteObstruction.c1830 line 167
  20. theorem OAI.BorsukNine.FiniteObstruction.c1831 line 177
  21. theorem OAI.BorsukNine.FiniteObstruction.c1832 line 187
  22. theorem OAI.BorsukNine.FiniteObstruction.c1833 line 197
  23. theorem OAI.BorsukNine.FiniteObstruction.c1834 line 207
  24. theorem OAI.BorsukNine.FiniteObstruction.c1835 line 217
  25. theorem OAI.BorsukNine.FiniteObstruction.c1836 line 227
  26. theorem OAI.BorsukNine.FiniteObstruction.c1837 line 237
  27. theorem OAI.BorsukNine.FiniteObstruction.c1838 line 247
  28. theorem OAI.BorsukNine.FiniteObstruction.c1840 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c1841 line 267
  30. theorem OAI.BorsukNine.FiniteObstruction.c1842 line 277
  31. theorem OAI.BorsukNine.FiniteObstruction.c1843 line 287
  32. theorem OAI.BorsukNine.FiniteObstruction.c1844 line 297
  33. theorem OAI.BorsukNine.FiniteObstruction.c1845 line 307
  34. theorem OAI.BorsukNine.FiniteObstruction.c1846 line 317
  35. theorem OAI.BorsukNine.FiniteObstruction.c1847 line 327
  36. theorem OAI.BorsukNine.FiniteObstruction.c1848 line 337
  37. theorem OAI.BorsukNine.FiniteObstruction.c1849 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c1850 line 357
  39. theorem OAI.BorsukNine.FiniteObstruction.c1851 line 367
  40. theorem OAI.BorsukNine.FiniteObstruction.c1852 line 377
  41. theorem OAI.BorsukNine.FiniteObstruction.c1853 line 387
  42. theorem OAI.BorsukNine.FiniteObstruction.c1854 line 397
  43. theorem OAI.BorsukNine.FiniteObstruction.c1855 line 407
  44. theorem OAI.BorsukNine.FiniteObstruction.c1856 line 417
  45. theorem OAI.BorsukNine.FiniteObstruction.c1857 line 427