OAI/Geometry/Borsuk/FiniteCases/Cases041.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c12311 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c12314 line 19
  3. theorem OAI.BorsukNine.FiniteObstruction.c12316 line 27
  4. theorem OAI.BorsukNine.FiniteObstruction.c12317 line 35
  5. theorem OAI.BorsukNine.FiniteObstruction.c12321 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c12327 line 51
  7. theorem OAI.BorsukNine.FiniteObstruction.c12328 line 61
  8. theorem OAI.BorsukNine.FiniteObstruction.c12331 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c12333 line 81
  10. theorem OAI.BorsukNine.FiniteObstruction.c12335 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c12336 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c12338 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c12341 line 121
  14. theorem OAI.BorsukNine.FiniteObstruction.c12354 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c12356 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c12363 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c12365 line 161
  18. theorem OAI.BorsukNine.FiniteObstruction.c12367 line 171
  19. theorem OAI.BorsukNine.FiniteObstruction.c12370 line 181
  20. theorem OAI.BorsukNine.FiniteObstruction.c12372 line 191
  21. theorem OAI.BorsukNine.FiniteObstruction.c12375 line 201
  22. theorem OAI.BorsukNine.FiniteObstruction.c12377 line 211
  23. theorem OAI.BorsukNine.FiniteObstruction.c12380 line 221
  24. theorem OAI.BorsukNine.FiniteObstruction.c12381 line 231
  25. theorem OAI.BorsukNine.FiniteObstruction.c12390 line 241
  26. theorem OAI.BorsukNine.FiniteObstruction.c12393 line 251
  27. theorem OAI.BorsukNine.FiniteObstruction.c12396 line 261
  28. theorem OAI.BorsukNine.FiniteObstruction.c12397 line 271
  29. theorem OAI.BorsukNine.FiniteObstruction.c12399 line 281
  30. theorem OAI.BorsukNine.FiniteObstruction.c12410 line 291
  31. theorem OAI.BorsukNine.FiniteObstruction.c12413 line 301
  32. theorem OAI.BorsukNine.FiniteObstruction.c12419 line 311
  33. theorem OAI.BorsukNine.FiniteObstruction.c12422 line 321
  34. theorem OAI.BorsukNine.FiniteObstruction.c12436 line 331
  35. theorem OAI.BorsukNine.FiniteObstruction.c12443 line 341
  36. theorem OAI.BorsukNine.FiniteObstruction.c12448 line 349
  37. theorem OAI.BorsukNine.FiniteObstruction.c12459 line 357
  38. theorem OAI.BorsukNine.FiniteObstruction.c12471 line 365
  39. theorem OAI.BorsukNine.FiniteObstruction.c12510 line 375
  40. theorem OAI.BorsukNine.FiniteObstruction.c12559 line 385
  41. theorem OAI.BorsukNine.FiniteObstruction.c12575 line 395
  42. theorem OAI.BorsukNine.FiniteObstruction.c12583 line 405
  43. theorem OAI.BorsukNine.FiniteObstruction.c12587 line 413
  44. theorem OAI.BorsukNine.FiniteObstruction.c12591 line 421
  45. theorem OAI.BorsukNine.FiniteObstruction.c12594 line 429