OAI/Geometry/Borsuk/FiniteCases/Cases015.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1350 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1352 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c1355 line 33
  4. theorem OAI.BorsukNine.FiniteObstruction.c1359 line 38
  5. theorem OAI.BorsukNine.FiniteObstruction.c1361 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c1362 line 48
  7. theorem OAI.BorsukNine.FiniteObstruction.c1366 line 65
  8. theorem OAI.BorsukNine.FiniteObstruction.c1367 line 82
  9. theorem OAI.BorsukNine.FiniteObstruction.c1376 line 99
  10. theorem OAI.BorsukNine.FiniteObstruction.c1382 line 104
  11. theorem OAI.BorsukNine.FiniteObstruction.c1383 line 121
  12. theorem OAI.BorsukNine.FiniteObstruction.c1384 line 126
  13. theorem OAI.BorsukNine.FiniteObstruction.c1386 line 143
  14. theorem OAI.BorsukNine.FiniteObstruction.c1388 line 160
  15. theorem OAI.BorsukNine.FiniteObstruction.c1389 line 177
  16. theorem OAI.BorsukNine.FiniteObstruction.c1390 line 182
  17. theorem OAI.BorsukNine.FiniteObstruction.c1391 line 199
  18. theorem OAI.BorsukNine.FiniteObstruction.c1392 line 204
  19. theorem OAI.BorsukNine.FiniteObstruction.c1393 line 221
  20. theorem OAI.BorsukNine.FiniteObstruction.c1394 line 226
  21. theorem OAI.BorsukNine.FiniteObstruction.c1395 line 243
  22. theorem OAI.BorsukNine.FiniteObstruction.c1396 line 248
  23. theorem OAI.BorsukNine.FiniteObstruction.c1397 line 265
  24. theorem OAI.BorsukNine.FiniteObstruction.c1399 line 282
  25. theorem OAI.BorsukNine.FiniteObstruction.c1400 line 299
  26. theorem OAI.BorsukNine.FiniteObstruction.c1405 line 304
  27. theorem OAI.BorsukNine.FiniteObstruction.c1410 line 321
  28. theorem OAI.BorsukNine.FiniteObstruction.c1411 line 326
  29. theorem OAI.BorsukNine.FiniteObstruction.c1412 line 343
  30. theorem OAI.BorsukNine.FiniteObstruction.c1413 line 360
  31. theorem OAI.BorsukNine.FiniteObstruction.c1419 line 365
  32. theorem OAI.BorsukNine.FiniteObstruction.c1420 line 370
  33. theorem OAI.BorsukNine.FiniteObstruction.c1422 line 387
  34. theorem OAI.BorsukNine.FiniteObstruction.c1424 line 404
  35. theorem OAI.BorsukNine.FiniteObstruction.c1425 line 421
  36. theorem OAI.BorsukNine.FiniteObstruction.c1426 line 426