OAI/Geometry/Borsuk/FiniteCases/Cases035.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c9181 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c9189 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c9203 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c9205 line 41
  5. theorem OAI.BorsukNine.FiniteObstruction.c9215 line 51
  6. theorem OAI.BorsukNine.FiniteObstruction.c9222 line 61
  7. theorem OAI.BorsukNine.FiniteObstruction.c9223 line 69
  8. theorem OAI.BorsukNine.FiniteObstruction.c9224 line 77
  9. theorem OAI.BorsukNine.FiniteObstruction.c9226 line 85
  10. theorem OAI.BorsukNine.FiniteObstruction.c9228 line 93
  11. theorem OAI.BorsukNine.FiniteObstruction.c9235 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c9237 line 109
  13. theorem OAI.BorsukNine.FiniteObstruction.c9273 line 117
  14. theorem OAI.BorsukNine.FiniteObstruction.c9291 line 127
  15. theorem OAI.BorsukNine.FiniteObstruction.c9318 line 137
  16. theorem OAI.BorsukNine.FiniteObstruction.c9320 line 147
  17. theorem OAI.BorsukNine.FiniteObstruction.c9330 line 157
  18. theorem OAI.BorsukNine.FiniteObstruction.c9333 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c9342 line 177
  20. theorem OAI.BorsukNine.FiniteObstruction.c9361 line 187
  21. theorem OAI.BorsukNine.FiniteObstruction.c9362 line 197
  22. theorem OAI.BorsukNine.FiniteObstruction.c9363 line 205
  23. theorem OAI.BorsukNine.FiniteObstruction.c9364 line 213
  24. theorem OAI.BorsukNine.FiniteObstruction.c9365 line 221
  25. theorem OAI.BorsukNine.FiniteObstruction.c9366 line 229
  26. theorem OAI.BorsukNine.FiniteObstruction.c9373 line 237
  27. theorem OAI.BorsukNine.FiniteObstruction.c9379 line 245
  28. theorem OAI.BorsukNine.FiniteObstruction.c9477 line 253
  29. theorem OAI.BorsukNine.FiniteObstruction.c9503 line 263
  30. theorem OAI.BorsukNine.FiniteObstruction.c9506 line 271
  31. theorem OAI.BorsukNine.FiniteObstruction.c9508 line 279
  32. theorem OAI.BorsukNine.FiniteObstruction.c9517 line 287
  33. theorem OAI.BorsukNine.FiniteObstruction.c9521 line 295
  34. theorem OAI.BorsukNine.FiniteObstruction.c9524 line 303
  35. theorem OAI.BorsukNine.FiniteObstruction.c9573 line 313
  36. theorem OAI.BorsukNine.FiniteObstruction.c9615 line 323
  37. theorem OAI.BorsukNine.FiniteObstruction.c9642 line 333
  38. theorem OAI.BorsukNine.FiniteObstruction.c9644 line 341
  39. theorem OAI.BorsukNine.FiniteObstruction.c9645 line 349
  40. theorem OAI.BorsukNine.FiniteObstruction.c9646 line 357
  41. theorem OAI.BorsukNine.FiniteObstruction.c9647 line 365
  42. theorem OAI.BorsukNine.FiniteObstruction.c9648 line 373
  43. theorem OAI.BorsukNine.FiniteObstruction.c9649 line 381
  44. theorem OAI.BorsukNine.FiniteObstruction.c9651 line 389
  45. theorem OAI.BorsukNine.FiniteObstruction.c9665 line 397
  46. theorem OAI.BorsukNine.FiniteObstruction.c9710 line 407
  47. theorem OAI.BorsukNine.FiniteObstruction.c9730 line 417
  48. theorem OAI.BorsukNine.FiniteObstruction.c9735 line 427