OAI/Geometry/Borsuk/FiniteCases/Cases055.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c19282 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c19303 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c19309 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c19316 line 37
  5. theorem OAI.BorsukNine.FiniteObstruction.c19317 line 45
  6. theorem OAI.BorsukNine.FiniteObstruction.c19320 line 53
  7. theorem OAI.BorsukNine.FiniteObstruction.c19323 line 61
  8. theorem OAI.BorsukNine.FiniteObstruction.c19325 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c19357 line 81
  10. theorem OAI.BorsukNine.FiniteObstruction.c19365 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c19413 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c19422 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c19435 line 121
  14. theorem OAI.BorsukNine.FiniteObstruction.c19449 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c19459 line 139
  16. theorem OAI.BorsukNine.FiniteObstruction.c19463 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c19475 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c19536 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c19583 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c19584 line 185
  21. theorem OAI.BorsukNine.FiniteObstruction.c19597 line 193
  22. theorem OAI.BorsukNine.FiniteObstruction.c19723 line 201
  23. theorem OAI.BorsukNine.FiniteObstruction.c19724 line 209
  24. theorem OAI.BorsukNine.FiniteObstruction.c19725 line 217
  25. theorem OAI.BorsukNine.FiniteObstruction.c19726 line 225
  26. theorem OAI.BorsukNine.FiniteObstruction.c19727 line 233
  27. theorem OAI.BorsukNine.FiniteObstruction.c19728 line 241
  28. theorem OAI.BorsukNine.FiniteObstruction.c19729 line 249
  29. theorem OAI.BorsukNine.FiniteObstruction.c19731 line 257
  30. theorem OAI.BorsukNine.FiniteObstruction.c19732 line 265
  31. theorem OAI.BorsukNine.FiniteObstruction.c19735 line 273
  32. theorem OAI.BorsukNine.FiniteObstruction.c19738 line 281
  33. theorem OAI.BorsukNine.FiniteObstruction.c19739 line 289
  34. theorem OAI.BorsukNine.FiniteObstruction.c19753 line 297
  35. theorem OAI.BorsukNine.FiniteObstruction.c19773 line 307
  36. theorem OAI.BorsukNine.FiniteObstruction.c19783 line 317
  37. theorem OAI.BorsukNine.FiniteObstruction.c19798 line 327
  38. theorem OAI.BorsukNine.FiniteObstruction.c19800 line 337
  39. theorem OAI.BorsukNine.FiniteObstruction.c19842 line 347
  40. theorem OAI.BorsukNine.FiniteObstruction.c19847 line 357
  41. theorem OAI.BorsukNine.FiniteObstruction.c19848 line 367
  42. theorem OAI.BorsukNine.FiniteObstruction.c19850 line 377
  43. theorem OAI.BorsukNine.FiniteObstruction.c19880 line 387
  44. theorem OAI.BorsukNine.FiniteObstruction.c19887 line 395
  45. theorem OAI.BorsukNine.FiniteObstruction.c19899 line 405
  46. theorem OAI.BorsukNine.FiniteObstruction.c19919 line 415
  47. theorem OAI.BorsukNine.FiniteObstruction.c19941 line 425