OAI/Geometry/Borsuk/FiniteCases/Cases145.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BorsukNine.FiniteObstruction.c32879 line 11
  2. theorem OAI.BorsukNine.FiniteObstruction.c32880 line 23
  3. theorem OAI.BorsukNine.FiniteObstruction.c32888 line 35
  4. theorem OAI.BorsukNine.FiniteObstruction.c32897 line 44
  5. theorem OAI.BorsukNine.FiniteObstruction.c32906 line 53
  6. theorem OAI.BorsukNine.FiniteObstruction.c32921 line 65
  7. theorem OAI.BorsukNine.FiniteObstruction.no_fixed_ten_system line 88
  8. theorem OAI.BorsukNine.FiniteObstruction.no_ten_system line 91