OAI/Geometry/Borsuk/FiniteCases/Cases075.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c29004 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c29025 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c29027 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c29032 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c29035 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c29057 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c29064 line 71
  8. theorem OAI.BorsukNine.FiniteObstruction.c29067 line 81
  9. theorem OAI.BorsukNine.FiniteObstruction.c29071 line 91
  10. theorem OAI.BorsukNine.FiniteObstruction.c29074 line 101
  11. theorem OAI.BorsukNine.FiniteObstruction.c29077 line 111
  12. theorem OAI.BorsukNine.FiniteObstruction.c29080 line 121
  13. theorem OAI.BorsukNine.FiniteObstruction.c29082 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c29087 line 141
  15. theorem OAI.BorsukNine.FiniteObstruction.c29095 line 151
  16. theorem OAI.BorsukNine.FiniteObstruction.c29098 line 161
  17. theorem OAI.BorsukNine.FiniteObstruction.c29100 line 171
  18. theorem OAI.BorsukNine.FiniteObstruction.c29123 line 181
  19. theorem OAI.BorsukNine.FiniteObstruction.c29131 line 191
  20. theorem OAI.BorsukNine.FiniteObstruction.c29139 line 201
  21. theorem OAI.BorsukNine.FiniteObstruction.c29146 line 211
  22. theorem OAI.BorsukNine.FiniteObstruction.c29263 line 221
  23. theorem OAI.BorsukNine.FiniteObstruction.c29271 line 231
  24. theorem OAI.BorsukNine.FiniteObstruction.c29279 line 241
  25. theorem OAI.BorsukNine.FiniteObstruction.c29286 line 251
  26. theorem OAI.BorsukNine.FiniteObstruction.c29403 line 261
  27. theorem OAI.BorsukNine.FiniteObstruction.c29411 line 271
  28. theorem OAI.BorsukNine.FiniteObstruction.c29419 line 281
  29. theorem OAI.BorsukNine.FiniteObstruction.c29426 line 291
  30. theorem OAI.BorsukNine.FiniteObstruction.c29543 line 301
  31. theorem OAI.BorsukNine.FiniteObstruction.c29551 line 311
  32. theorem OAI.BorsukNine.FiniteObstruction.c29559 line 321
  33. theorem OAI.BorsukNine.FiniteObstruction.c29566 line 331
  34. theorem OAI.BorsukNine.FiniteObstruction.c29683 line 341
  35. theorem OAI.BorsukNine.FiniteObstruction.c29691 line 351
  36. theorem OAI.BorsukNine.FiniteObstruction.c29699 line 361
  37. theorem OAI.BorsukNine.FiniteObstruction.c29706 line 371
  38. theorem OAI.BorsukNine.FiniteObstruction.c29823 line 381
  39. theorem OAI.BorsukNine.FiniteObstruction.c29831 line 391
  40. theorem OAI.BorsukNine.FiniteObstruction.c29839 line 401
  41. theorem OAI.BorsukNine.FiniteObstruction.c29846 line 411
  42. theorem OAI.BorsukNine.FiniteObstruction.c29963 line 421