OAI/Geometry/Borsuk/FiniteCases/Cases011.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c913 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c916 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c917 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c922 line 50
  5. theorem OAI.BorsukNine.FiniteObstruction.c926 line 55
  6. theorem OAI.BorsukNine.FiniteObstruction.c928 line 60
  7. theorem OAI.BorsukNine.FiniteObstruction.c929 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c931 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c932 line 99
  10. theorem OAI.BorsukNine.FiniteObstruction.c934 line 116
  11. theorem OAI.BorsukNine.FiniteObstruction.c937 line 133
  12. theorem OAI.BorsukNine.FiniteObstruction.c939 line 138
  13. theorem OAI.BorsukNine.FiniteObstruction.c940 line 143
  14. theorem OAI.BorsukNine.FiniteObstruction.c941 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c943 line 165
  16. theorem OAI.BorsukNine.FiniteObstruction.c944 line 170
  17. theorem OAI.BorsukNine.FiniteObstruction.c946 line 187
  18. theorem OAI.BorsukNine.FiniteObstruction.c947 line 204
  19. theorem OAI.BorsukNine.FiniteObstruction.c949 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c950 line 238
  21. theorem OAI.BorsukNine.FiniteObstruction.c952 line 243
  22. theorem OAI.BorsukNine.FiniteObstruction.c954 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c955 line 253
  24. theorem OAI.BorsukNine.FiniteObstruction.c956 line 270
  25. theorem OAI.BorsukNine.FiniteObstruction.c958 line 275
  26. theorem OAI.BorsukNine.FiniteObstruction.c962 line 280
  27. theorem OAI.BorsukNine.FiniteObstruction.c963 line 297
  28. theorem OAI.BorsukNine.FiniteObstruction.c968 line 302
  29. theorem OAI.BorsukNine.FiniteObstruction.c969 line 319
  30. theorem OAI.BorsukNine.FiniteObstruction.c970 line 324
  31. theorem OAI.BorsukNine.FiniteObstruction.c971 line 341
  32. theorem OAI.BorsukNine.FiniteObstruction.c972 line 346
  33. theorem OAI.BorsukNine.FiniteObstruction.c975 line 363
  34. theorem OAI.BorsukNine.FiniteObstruction.c977 line 368
  35. theorem OAI.BorsukNine.FiniteObstruction.c983 line 385
  36. theorem OAI.BorsukNine.FiniteObstruction.c985 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c988 line 419
  38. theorem OAI.BorsukNine.FiniteObstruction.c990 line 424
  39. theorem OAI.BorsukNine.FiniteObstruction.c992 line 429