OAI/Geometry/Borsuk/FiniteCases/Cases074.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c28768 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c28776 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c28781 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c28799 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c28800 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c28802 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c28804 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c28815 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c28816 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c28818 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c28823 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c28826 line 119
  13. theorem OAI.BorsukNine.FiniteObstruction.c28829 line 127
  14. theorem OAI.BorsukNine.FiniteObstruction.c28830 line 135
  15. theorem OAI.BorsukNine.FiniteObstruction.c28836 line 143
  16. theorem OAI.BorsukNine.FiniteObstruction.c28837 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c28838 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c28840 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c28841 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c28845 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c28853 line 193
  22. theorem OAI.BorsukNine.FiniteObstruction.c28855 line 203
  23. theorem OAI.BorsukNine.FiniteObstruction.c28887 line 213
  24. theorem OAI.BorsukNine.FiniteObstruction.c28891 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c28924 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c28931 line 243
  27. theorem OAI.BorsukNine.FiniteObstruction.c28947 line 253
  28. theorem OAI.BorsukNine.FiniteObstruction.c28963 line 263
  29. theorem OAI.BorsukNine.FiniteObstruction.c28964 line 271
  30. theorem OAI.BorsukNine.FiniteObstruction.c28965 line 279
  31. theorem OAI.BorsukNine.FiniteObstruction.c28966 line 287
  32. theorem OAI.BorsukNine.FiniteObstruction.c28968 line 295
  33. theorem OAI.BorsukNine.FiniteObstruction.c28969 line 303
  34. theorem OAI.BorsukNine.FiniteObstruction.c28971 line 311
  35. theorem OAI.BorsukNine.FiniteObstruction.c28972 line 319
  36. theorem OAI.BorsukNine.FiniteObstruction.c28975 line 327
  37. theorem OAI.BorsukNine.FiniteObstruction.c28976 line 335
  38. theorem OAI.BorsukNine.FiniteObstruction.c28978 line 343
  39. theorem OAI.BorsukNine.FiniteObstruction.c28980 line 351
  40. theorem OAI.BorsukNine.FiniteObstruction.c28981 line 359
  41. theorem OAI.BorsukNine.FiniteObstruction.c28983 line 367
  42. theorem OAI.BorsukNine.FiniteObstruction.c28985 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c28988 line 387
  44. theorem OAI.BorsukNine.FiniteObstruction.c28995 line 397
  45. theorem OAI.BorsukNine.FiniteObstruction.c28998 line 407
  46. theorem OAI.BorsukNine.FiniteObstruction.c29001 line 417
  47. theorem OAI.BorsukNine.FiniteObstruction.c29002 line 427