OAI/Geometry/Borsuk/FiniteCases/Cases038.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c10870 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c10903 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c10925 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c10933 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c10935 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c10965 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c11012 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c11013 line 79
  9. theorem OAI.BorsukNine.FiniteObstruction.c11032 line 89
  10. theorem OAI.BorsukNine.FiniteObstruction.c11043 line 99
  11. theorem OAI.BorsukNine.FiniteObstruction.c11048 line 107
  12. theorem OAI.BorsukNine.FiniteObstruction.c11052 line 115
  13. theorem OAI.BorsukNine.FiniteObstruction.c11054 line 123
  14. theorem OAI.BorsukNine.FiniteObstruction.c11058 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c11061 line 139
  16. theorem OAI.BorsukNine.FiniteObstruction.c11065 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c11067 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c11068 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c11073 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c11075 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c11076 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c11087 line 207
  23. theorem OAI.BorsukNine.FiniteObstruction.c11097 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c11115 line 227
  25. theorem OAI.BorsukNine.FiniteObstruction.c11119 line 237
  26. theorem OAI.BorsukNine.FiniteObstruction.c11133 line 247
  27. theorem OAI.BorsukNine.FiniteObstruction.c11134 line 257
  28. theorem OAI.BorsukNine.FiniteObstruction.c11150 line 267
  29. theorem OAI.BorsukNine.FiniteObstruction.c11152 line 277
  30. theorem OAI.BorsukNine.FiniteObstruction.c11153 line 287
  31. theorem OAI.BorsukNine.FiniteObstruction.c11168 line 297
  32. theorem OAI.BorsukNine.FiniteObstruction.c11183 line 307
  33. theorem OAI.BorsukNine.FiniteObstruction.c11211 line 315
  34. theorem OAI.BorsukNine.FiniteObstruction.c11315 line 325
  35. theorem OAI.BorsukNine.FiniteObstruction.c11323 line 335
  36. theorem OAI.BorsukNine.FiniteObstruction.c11325 line 343
  37. theorem OAI.BorsukNine.FiniteObstruction.c11326 line 351
  38. theorem OAI.BorsukNine.FiniteObstruction.c11328 line 359
  39. theorem OAI.BorsukNine.FiniteObstruction.c11329 line 367
  40. theorem OAI.BorsukNine.FiniteObstruction.c11330 line 375
  41. theorem OAI.BorsukNine.FiniteObstruction.c11334 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c11336 line 391
  43. theorem OAI.BorsukNine.FiniteObstruction.c11337 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c11339 line 407
  45. theorem OAI.BorsukNine.FiniteObstruction.c11341 line 415
  46. theorem OAI.BorsukNine.FiniteObstruction.c11345 line 423