OAI/Geometry/Borsuk/FiniteCases/Cases050.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c17174 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c17176 line 21
  3. theorem OAI.BorsukNine.FiniteObstruction.c17203 line 31
  4. theorem OAI.BorsukNine.FiniteObstruction.c17205 line 39
  5. theorem OAI.BorsukNine.FiniteObstruction.c17207 line 47
  6. theorem OAI.BorsukNine.FiniteObstruction.c17211 line 55
  7. theorem OAI.BorsukNine.FiniteObstruction.c17219 line 63
  8. theorem OAI.BorsukNine.FiniteObstruction.c17240 line 71
  9. theorem OAI.BorsukNine.FiniteObstruction.c17255 line 81
  10. theorem OAI.BorsukNine.FiniteObstruction.c17257 line 91
  11. theorem OAI.BorsukNine.FiniteObstruction.c17297 line 101
  12. theorem OAI.BorsukNine.FiniteObstruction.c17298 line 111
  13. theorem OAI.BorsukNine.FiniteObstruction.c17299 line 121
  14. theorem OAI.BorsukNine.FiniteObstruction.c17315 line 131
  15. theorem OAI.BorsukNine.FiniteObstruction.c17331 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c17342 line 151
  17. theorem OAI.BorsukNine.FiniteObstruction.c17343 line 159
  18. theorem OAI.BorsukNine.FiniteObstruction.c17344 line 167
  19. theorem OAI.BorsukNine.FiniteObstruction.c17346 line 175
  20. theorem OAI.BorsukNine.FiniteObstruction.c17351 line 183
  21. theorem OAI.BorsukNine.FiniteObstruction.c17357 line 191
  22. theorem OAI.BorsukNine.FiniteObstruction.c17361 line 199
  23. theorem OAI.BorsukNine.FiniteObstruction.c17365 line 207
  24. theorem OAI.BorsukNine.FiniteObstruction.c17373 line 217
  25. theorem OAI.BorsukNine.FiniteObstruction.c17378 line 227
  26. theorem OAI.BorsukNine.FiniteObstruction.c17387 line 237
  27. theorem OAI.BorsukNine.FiniteObstruction.c17426 line 247
  28. theorem OAI.BorsukNine.FiniteObstruction.c17437 line 257
  29. theorem OAI.BorsukNine.FiniteObstruction.c17483 line 267
  30. theorem OAI.BorsukNine.FiniteObstruction.c17484 line 275
  31. theorem OAI.BorsukNine.FiniteObstruction.c17485 line 283
  32. theorem OAI.BorsukNine.FiniteObstruction.c17487 line 291
  33. theorem OAI.BorsukNine.FiniteObstruction.c17493 line 299
  34. theorem OAI.BorsukNine.FiniteObstruction.c17511 line 307
  35. theorem OAI.BorsukNine.FiniteObstruction.c17535 line 317
  36. theorem OAI.BorsukNine.FiniteObstruction.c17537 line 327
  37. theorem OAI.BorsukNine.FiniteObstruction.c17552 line 337
  38. theorem OAI.BorsukNine.FiniteObstruction.c17575 line 347
  39. theorem OAI.BorsukNine.FiniteObstruction.c17576 line 357
  40. theorem OAI.BorsukNine.FiniteObstruction.c17577 line 367
  41. theorem OAI.BorsukNine.FiniteObstruction.c17578 line 377
  42. theorem OAI.BorsukNine.FiniteObstruction.c17579 line 387
  43. theorem OAI.BorsukNine.FiniteObstruction.c17581 line 397
  44. theorem OAI.BorsukNine.FiniteObstruction.c17583 line 407
  45. theorem OAI.BorsukNine.FiniteObstruction.c17585 line 417
  46. theorem OAI.BorsukNine.FiniteObstruction.c17586 line 427