OAI/Geometry/Borsuk/FiniteCases/Cases065.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c24639 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c24643 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c24647 line 29
  4. theorem OAI.BorsukNine.FiniteObstruction.c24653 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c24703 line 49
  6. theorem OAI.BorsukNine.FiniteObstruction.c24724 line 59
  7. theorem OAI.BorsukNine.FiniteObstruction.c24742 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c24747 line 79
  9. theorem OAI.BorsukNine.FiniteObstruction.c24748 line 89
  10. theorem OAI.BorsukNine.FiniteObstruction.c24750 line 99
  11. theorem OAI.BorsukNine.FiniteObstruction.c24785 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c24803 line 119
  13. theorem OAI.BorsukNine.FiniteObstruction.c24827 line 129
  14. theorem OAI.BorsukNine.FiniteObstruction.c24895 line 139
  15. theorem OAI.BorsukNine.FiniteObstruction.c24903 line 149
  16. theorem OAI.BorsukNine.FiniteObstruction.c24916 line 157
  17. theorem OAI.BorsukNine.FiniteObstruction.c24965 line 165
  18. theorem OAI.BorsukNine.FiniteObstruction.c24967 line 175
  19. theorem OAI.BorsukNine.FiniteObstruction.c25043 line 185
  20. theorem OAI.BorsukNine.FiniteObstruction.c25045 line 193
  21. theorem OAI.BorsukNine.FiniteObstruction.c25048 line 201
  22. theorem OAI.BorsukNine.FiniteObstruction.c25049 line 209
  23. theorem OAI.BorsukNine.FiniteObstruction.c25056 line 217
  24. theorem OAI.BorsukNine.FiniteObstruction.c25057 line 225
  25. theorem OAI.BorsukNine.FiniteObstruction.c25073 line 233
  26. theorem OAI.BorsukNine.FiniteObstruction.c25075 line 243
  27. theorem OAI.BorsukNine.FiniteObstruction.c25097 line 253
  28. theorem OAI.BorsukNine.FiniteObstruction.c25107 line 263
  29. theorem OAI.BorsukNine.FiniteObstruction.c25126 line 273
  30. theorem OAI.BorsukNine.FiniteObstruction.c25131 line 283
  31. theorem OAI.BorsukNine.FiniteObstruction.c25150 line 293
  32. theorem OAI.BorsukNine.FiniteObstruction.c25159 line 303
  33. theorem OAI.BorsukNine.FiniteObstruction.c25162 line 313
  34. theorem OAI.BorsukNine.FiniteObstruction.c25183 line 323
  35. theorem OAI.BorsukNine.FiniteObstruction.c25188 line 331
  36. theorem OAI.BorsukNine.FiniteObstruction.c25196 line 339
  37. theorem OAI.BorsukNine.FiniteObstruction.c25215 line 347
  38. theorem OAI.BorsukNine.FiniteObstruction.c25243 line 357
  39. theorem OAI.BorsukNine.FiniteObstruction.c25329 line 367
  40. theorem OAI.BorsukNine.FiniteObstruction.c25334 line 375
  41. theorem OAI.BorsukNine.FiniteObstruction.c25335 line 383
  42. theorem OAI.BorsukNine.FiniteObstruction.c25336 line 391
  43. theorem OAI.BorsukNine.FiniteObstruction.c25351 line 399
  44. theorem OAI.BorsukNine.FiniteObstruction.c25355 line 409
  45. theorem OAI.BorsukNine.FiniteObstruction.c25368 line 419
  46. theorem OAI.BorsukNine.FiniteObstruction.c25385 line 429