OAI/Geometry/SingularHomology/SingularUniversalChainMap.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SingularUniversalOperator.faceMap line 14
  2. def OAI.Problem340.SingularUniversalOperator.faceSum line 17
  3. theorem OAI.Problem340.SingularUniversalOperator.operator_identity_apply line 22
  4. theorem OAI.Problem340.SingularUniversalOperator.operator_identity_boundary line 29
  5. def OAI.Problem340.SingularUniversalOperator.BoundaryCompatible line 46
  6. theorem OAI.Problem340.SingularUniversalOperator.operator_comm line 50
  7. def OAI.Problem340.SingularUniversalOperator.chainMap line 64
  8. theorem OAI.Problem340.SingularUniversalOperator.chainMap_app_f line 69
  9. theorem OAI.Problem340.SingularUniversalOperator.chainMap_zero line 73
  10. def OAI.Problem340.SingularUniversalOperator.chainMapHomotopy line 82
  11. theorem OAI.Problem340.SingularUniversalOperator.chainMapHomotopy_naturality line 87
  12. theorem OAI.Problem340.SingularUniversalOperator.chainMap_homologyMap_eq_id line 97