OAI/Geometry/Borsuk/FiniteCases/Cases046.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c14299 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c14315 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c14330 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c14331 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c14332 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c14338 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c14339 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c14342 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c14343 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c14370 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c14373 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c14374 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c14404 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c14497 line 139
  15. theorem OAI.BorsukNine.FiniteObstruction.c14544 line 149
  16. theorem OAI.BorsukNine.FiniteObstruction.c14549 line 157
  17. theorem OAI.BorsukNine.FiniteObstruction.c14597 line 165
  18. theorem OAI.BorsukNine.FiniteObstruction.c14645 line 175
  19. theorem OAI.BorsukNine.FiniteObstruction.c14681 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c14685 line 195
  21. theorem OAI.BorsukNine.FiniteObstruction.c14689 line 203
  22. theorem OAI.BorsukNine.FiniteObstruction.c14786 line 211
  23. theorem OAI.BorsukNine.FiniteObstruction.c14804 line 221
  24. theorem OAI.BorsukNine.FiniteObstruction.c14826 line 231
  25. theorem OAI.BorsukNine.FiniteObstruction.c14828 line 239
  26. theorem OAI.BorsukNine.FiniteObstruction.c14937 line 247
  27. theorem OAI.BorsukNine.FiniteObstruction.c14941 line 257
  28. theorem OAI.BorsukNine.FiniteObstruction.c14945 line 267
  29. theorem OAI.BorsukNine.FiniteObstruction.c14966 line 277
  30. theorem OAI.BorsukNine.FiniteObstruction.c14967 line 285
  31. theorem OAI.BorsukNine.FiniteObstruction.c14975 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c14977 line 301
  33. theorem OAI.BorsukNine.FiniteObstruction.c15071 line 309
  34. theorem OAI.BorsukNine.FiniteObstruction.c15072 line 319
  35. theorem OAI.BorsukNine.FiniteObstruction.c15077 line 329
  36. theorem OAI.BorsukNine.FiniteObstruction.c15104 line 339
  37. theorem OAI.BorsukNine.FiniteObstruction.c15119 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c15155 line 355
  39. theorem OAI.BorsukNine.FiniteObstruction.c15169 line 365
  40. theorem OAI.BorsukNine.FiniteObstruction.c15187 line 375
  41. theorem OAI.BorsukNine.FiniteObstruction.c15215 line 385
  42. theorem OAI.BorsukNine.FiniteObstruction.c15231 line 395
  43. theorem OAI.BorsukNine.FiniteObstruction.c15242 line 405
  44. theorem OAI.BorsukNine.FiniteObstruction.c15246 line 413
  45. theorem OAI.BorsukNine.FiniteObstruction.c15250 line 421
  46. theorem OAI.BorsukNine.FiniteObstruction.c15257 line 429