OAI/Geometry/Borsuk/FiniteCases/Cases013.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c1117 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c1121 line 16
  3. theorem OAI.BorsukNine.FiniteObstruction.c1123 line 21
  4. theorem OAI.BorsukNine.FiniteObstruction.c1127 line 26
  5. theorem OAI.BorsukNine.FiniteObstruction.c1128 line 43
  6. theorem OAI.BorsukNine.FiniteObstruction.c1134 line 48
  7. theorem OAI.BorsukNine.FiniteObstruction.c1136 line 53
  8. theorem OAI.BorsukNine.FiniteObstruction.c1139 line 58
  9. theorem OAI.BorsukNine.FiniteObstruction.c1141 line 75
  10. theorem OAI.BorsukNine.FiniteObstruction.c1157 line 92
  11. theorem OAI.BorsukNine.FiniteObstruction.c1158 line 109
  12. theorem OAI.BorsukNine.FiniteObstruction.c1162 line 114
  13. theorem OAI.BorsukNine.FiniteObstruction.c1165 line 119
  14. theorem OAI.BorsukNine.FiniteObstruction.c1166 line 136
  15. theorem OAI.BorsukNine.FiniteObstruction.c1167 line 141
  16. theorem OAI.BorsukNine.FiniteObstruction.c1170 line 158
  17. theorem OAI.BorsukNine.FiniteObstruction.c1171 line 163
  18. theorem OAI.BorsukNine.FiniteObstruction.c1172 line 180
  19. theorem OAI.BorsukNine.FiniteObstruction.c1176 line 197
  20. theorem OAI.BorsukNine.FiniteObstruction.c1184 line 214
  21. theorem OAI.BorsukNine.FiniteObstruction.c1185 line 231
  22. theorem OAI.BorsukNine.FiniteObstruction.c1186 line 236
  23. theorem OAI.BorsukNine.FiniteObstruction.c1187 line 253
  24. theorem OAI.BorsukNine.FiniteObstruction.c1196 line 270
  25. theorem OAI.BorsukNine.FiniteObstruction.c1201 line 275
  26. theorem OAI.BorsukNine.FiniteObstruction.c1202 line 292
  27. theorem OAI.BorsukNine.FiniteObstruction.c1209 line 309
  28. theorem OAI.BorsukNine.FiniteObstruction.c1210 line 314
  29. theorem OAI.BorsukNine.FiniteObstruction.c1216 line 331
  30. theorem OAI.BorsukNine.FiniteObstruction.c1217 line 348
  31. theorem OAI.BorsukNine.FiniteObstruction.c1218 line 365
  32. theorem OAI.BorsukNine.FiniteObstruction.c1222 line 370
  33. theorem OAI.BorsukNine.FiniteObstruction.c1230 line 375
  34. theorem OAI.BorsukNine.FiniteObstruction.c1247 line 380
  35. theorem OAI.BorsukNine.FiniteObstruction.c1248 line 397
  36. theorem OAI.BorsukNine.FiniteObstruction.c1252 line 402
  37. theorem OAI.BorsukNine.FiniteObstruction.c1254 line 407
  38. theorem OAI.BorsukNine.FiniteObstruction.c1258 line 412
  39. theorem OAI.BorsukNine.FiniteObstruction.c1262 line 417