OAI/Geometry/Borsuk/FiniteCases/Cases003.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c226 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c227 line 28
  3. theorem OAI.BorsukNine.FiniteObstruction.c228 line 45
  4. theorem OAI.BorsukNine.FiniteObstruction.c231 line 50
  5. theorem OAI.BorsukNine.FiniteObstruction.c236 line 67
  6. theorem OAI.BorsukNine.FiniteObstruction.c241 line 72
  7. theorem OAI.BorsukNine.FiniteObstruction.c253 line 89
  8. theorem OAI.BorsukNine.FiniteObstruction.c254 line 94
  9. theorem OAI.BorsukNine.FiniteObstruction.c257 line 111
  10. theorem OAI.BorsukNine.FiniteObstruction.c258 line 128
  11. theorem OAI.BorsukNine.FiniteObstruction.c263 line 133
  12. theorem OAI.BorsukNine.FiniteObstruction.c264 line 150
  13. theorem OAI.BorsukNine.FiniteObstruction.c266 line 155
  14. theorem OAI.BorsukNine.FiniteObstruction.c268 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c271 line 165
  16. theorem OAI.BorsukNine.FiniteObstruction.c272 line 182
  17. theorem OAI.BorsukNine.FiniteObstruction.c276 line 199
  18. theorem OAI.BorsukNine.FiniteObstruction.c279 line 216
  19. theorem OAI.BorsukNine.FiniteObstruction.c281 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c282 line 226
  21. theorem OAI.BorsukNine.FiniteObstruction.c283 line 243
  22. theorem OAI.BorsukNine.FiniteObstruction.c284 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c285 line 265
  24. theorem OAI.BorsukNine.FiniteObstruction.c286 line 270
  25. theorem OAI.BorsukNine.FiniteObstruction.c287 line 287
  26. theorem OAI.BorsukNine.FiniteObstruction.c291 line 304
  27. theorem OAI.BorsukNine.FiniteObstruction.c292 line 321
  28. theorem OAI.BorsukNine.FiniteObstruction.c293 line 326
  29. theorem OAI.BorsukNine.FiniteObstruction.c294 line 343
  30. theorem OAI.BorsukNine.FiniteObstruction.c295 line 348
  31. theorem OAI.BorsukNine.FiniteObstruction.c296 line 365
  32. theorem OAI.BorsukNine.FiniteObstruction.c298 line 370
  33. theorem OAI.BorsukNine.FiniteObstruction.c300 line 375
  34. theorem OAI.BorsukNine.FiniteObstruction.c302 line 380
  35. theorem OAI.BorsukNine.FiniteObstruction.c303 line 397
  36. theorem OAI.BorsukNine.FiniteObstruction.c305 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c306 line 407
  38. theorem OAI.BorsukNine.FiniteObstruction.c307 line 424
  39. theorem OAI.BorsukNine.FiniteObstruction.c308 line 429