OAI/Geometry/Borsuk/FiniteCases/Cases014.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1270 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1271 line 28
  3. theorem OAI.BorsukNine.FiniteObstruction.c1273 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c1275 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c1281 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c1284 line 60
  7. theorem OAI.BorsukNine.FiniteObstruction.c1286 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c1288 line 70
  9. theorem OAI.BorsukNine.FiniteObstruction.c1292 line 75
  10. theorem OAI.BorsukNine.FiniteObstruction.c1296 line 92
  11. theorem OAI.BorsukNine.FiniteObstruction.c1297 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c1298 line 114
  13. theorem OAI.BorsukNine.FiniteObstruction.c1299 line 131
  14. theorem OAI.BorsukNine.FiniteObstruction.c1300 line 136
  15. theorem OAI.BorsukNine.FiniteObstruction.c1301 line 153
  16. theorem OAI.BorsukNine.FiniteObstruction.c1302 line 158
  17. theorem OAI.BorsukNine.FiniteObstruction.c1304 line 175
  18. theorem OAI.BorsukNine.FiniteObstruction.c1305 line 192
  19. theorem OAI.BorsukNine.FiniteObstruction.c1306 line 197
  20. theorem OAI.BorsukNine.FiniteObstruction.c1307 line 214
  21. theorem OAI.BorsukNine.FiniteObstruction.c1309 line 231
  22. theorem OAI.BorsukNine.FiniteObstruction.c1314 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c1316 line 253
  24. theorem OAI.BorsukNine.FiniteObstruction.c1317 line 258
  25. theorem OAI.BorsukNine.FiniteObstruction.c1319 line 275
  26. theorem OAI.BorsukNine.FiniteObstruction.c1320 line 292
  27. theorem OAI.BorsukNine.FiniteObstruction.c1322 line 297
  28. theorem OAI.BorsukNine.FiniteObstruction.c1329 line 314
  29. theorem OAI.BorsukNine.FiniteObstruction.c1332 line 319
  30. theorem OAI.BorsukNine.FiniteObstruction.c1335 line 336
  31. theorem OAI.BorsukNine.FiniteObstruction.c1337 line 341
  32. theorem OAI.BorsukNine.FiniteObstruction.c1340 line 358
  33. theorem OAI.BorsukNine.FiniteObstruction.c1341 line 363
  34. theorem OAI.BorsukNine.FiniteObstruction.c1343 line 380
  35. theorem OAI.BorsukNine.FiniteObstruction.c1346 line 397
  36. theorem OAI.BorsukNine.FiniteObstruction.c1347 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c1348 line 419
  38. theorem OAI.BorsukNine.FiniteObstruction.c1349 line 424