OAI/Geometry/Borsuk/FiniteCases/Cases010.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c838 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c839 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c841 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c842 line 50
  5. theorem OAI.BorsukNine.FiniteObstruction.c843 line 67
  6. theorem OAI.BorsukNine.FiniteObstruction.c844 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c846 line 89
  8. theorem OAI.BorsukNine.FiniteObstruction.c847 line 106
  9. theorem OAI.BorsukNine.FiniteObstruction.c850 line 111
  10. theorem OAI.BorsukNine.FiniteObstruction.c851 line 128
  11. theorem OAI.BorsukNine.FiniteObstruction.c853 line 133
  12. theorem OAI.BorsukNine.FiniteObstruction.c854 line 138
  13. theorem OAI.BorsukNine.FiniteObstruction.c855 line 155
  14. theorem OAI.BorsukNine.FiniteObstruction.c857 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c859 line 177
  16. theorem OAI.BorsukNine.FiniteObstruction.c860 line 194
  17. theorem OAI.BorsukNine.FiniteObstruction.c862 line 199
  18. theorem OAI.BorsukNine.FiniteObstruction.c865 line 204
  19. theorem OAI.BorsukNine.FiniteObstruction.c866 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c868 line 226
  21. theorem OAI.BorsukNine.FiniteObstruction.c870 line 231
  22. theorem OAI.BorsukNine.FiniteObstruction.c879 line 236
  23. theorem OAI.BorsukNine.FiniteObstruction.c880 line 241
  24. theorem OAI.BorsukNine.FiniteObstruction.c881 line 258
  25. theorem OAI.BorsukNine.FiniteObstruction.c882 line 263
  26. theorem OAI.BorsukNine.FiniteObstruction.c883 line 280
  27. theorem OAI.BorsukNine.FiniteObstruction.c885 line 285
  28. theorem OAI.BorsukNine.FiniteObstruction.c886 line 290
  29. theorem OAI.BorsukNine.FiniteObstruction.c887 line 307
  30. theorem OAI.BorsukNine.FiniteObstruction.c889 line 324
  31. theorem OAI.BorsukNine.FiniteObstruction.c894 line 341
  32. theorem OAI.BorsukNine.FiniteObstruction.c896 line 346
  33. theorem OAI.BorsukNine.FiniteObstruction.c901 line 351
  34. theorem OAI.BorsukNine.FiniteObstruction.c902 line 368
  35. theorem OAI.BorsukNine.FiniteObstruction.c903 line 385
  36. theorem OAI.BorsukNine.FiniteObstruction.c907 line 390
  37. theorem OAI.BorsukNine.FiniteObstruction.c909 line 395
  38. theorem OAI.BorsukNine.FiniteObstruction.c910 line 400
  39. theorem OAI.BorsukNine.FiniteObstruction.c912 line 417