OAI/Geometry/Borsuk/FiniteCases/Cases069.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c27117 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c27122 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c27135 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c27143 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c27151 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c27152 line 57
  7. theorem OAI.BorsukNine.FiniteObstruction.c27155 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c27158 line 73
  9. theorem OAI.BorsukNine.FiniteObstruction.c27159 line 81
  10. theorem OAI.BorsukNine.FiniteObstruction.c27160 line 89
  11. theorem OAI.BorsukNine.FiniteObstruction.c27171 line 97
  12. theorem OAI.BorsukNine.FiniteObstruction.c27175 line 107
  13. theorem OAI.BorsukNine.FiniteObstruction.c27176 line 117
  14. theorem OAI.BorsukNine.FiniteObstruction.c27205 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c27267 line 137
  16. theorem OAI.BorsukNine.FiniteObstruction.c27268 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c27292 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c27300 line 165
  19. theorem OAI.BorsukNine.FiniteObstruction.c27311 line 173
  20. theorem OAI.BorsukNine.FiniteObstruction.c27315 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c27328 line 193
  22. theorem OAI.BorsukNine.FiniteObstruction.c27335 line 203
  23. theorem OAI.BorsukNine.FiniteObstruction.c27347 line 213
  24. theorem OAI.BorsukNine.FiniteObstruction.c27351 line 223
  25. theorem OAI.BorsukNine.FiniteObstruction.c27423 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c27424 line 241
  27. theorem OAI.BorsukNine.FiniteObstruction.c27426 line 249
  28. theorem OAI.BorsukNine.FiniteObstruction.c27427 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c27428 line 265
  30. theorem OAI.BorsukNine.FiniteObstruction.c27433 line 273
  31. theorem OAI.BorsukNine.FiniteObstruction.c27434 line 281
  32. theorem OAI.BorsukNine.FiniteObstruction.c27435 line 289
  33. theorem OAI.BorsukNine.FiniteObstruction.c27437 line 297
  34. theorem OAI.BorsukNine.FiniteObstruction.c27438 line 305
  35. theorem OAI.BorsukNine.FiniteObstruction.c27439 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c27440 line 321
  37. theorem OAI.BorsukNine.FiniteObstruction.c27441 line 329
  38. theorem OAI.BorsukNine.FiniteObstruction.c27447 line 337
  39. theorem OAI.BorsukNine.FiniteObstruction.c27466 line 347
  40. theorem OAI.BorsukNine.FiniteObstruction.c27468 line 357
  41. theorem OAI.BorsukNine.FiniteObstruction.c27478 line 367
  42. theorem OAI.BorsukNine.FiniteObstruction.c27479 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c27481 line 387
  44. theorem OAI.BorsukNine.FiniteObstruction.c27483 line 397
  45. theorem OAI.BorsukNine.FiniteObstruction.c27487 line 407
  46. theorem OAI.BorsukNine.FiniteObstruction.c27488 line 417
  47. theorem OAI.BorsukNine.FiniteObstruction.c27491 line 427