OAI/Geometry/SingularHomology/SphereSquareHomologyTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.rawSphereSquare_eq_conjugate_standard line 14
  2. theorem OAI.Problem340.rawSphereSquare_eigenvector_of_standard line 21
  3. abbrev OAI.Problem340.StandardBase line 31
  4. def OAI.Problem340.standardBaseSquare line 33
  5. theorem OAI.Problem340.continuous_standardBaseSquare line 36
  6. def OAI.Problem340.baseHomeomorph line 39
  7. theorem OAI.Problem340.rawBaseSquare_eq_conjugate_standard line 42
  8. theorem OAI.Problem340.bddAbove_rawBaseSquare_of_standard line 53