OAI/Geometry/SingularHomology/SingularUniversalOperator.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SingularUniversalOperator.chainsFunctor line 12
  2. abbrev OAI.Problem340.SingularUniversalOperator.simplex line 16
  3. def OAI.Problem340.SingularUniversalOperator.simplexMap line 18
  4. theorem OAI.Problem340.SingularUniversalOperator.simplexMap_naturality line 22
  5. theorem OAI.Problem340.SingularUniversalOperator.generator_map line 28
  6. def OAI.Problem340.SingularUniversalOperator.operator line 37
  7. theorem OAI.Problem340.SingularUniversalOperator.generator_operator line 52
  8. theorem OAI.Problem340.SingularUniversalOperator.operator_generator_apply line 60
  9. def OAI.Problem340.SingularUniversalOperator.identitySimplex line 70
  10. theorem OAI.Problem340.SingularUniversalOperator.simplexMap_identity line 74
  11. def OAI.Problem340.SingularUniversalOperator.identityGenerator line 77
  12. theorem OAI.Problem340.SingularUniversalOperator.map_identitySimplex line 81
  13. theorem OAI.Problem340.SingularUniversalOperator.identityGenerator_map line 88
  14. theorem OAI.Problem340.SingularUniversalOperator.natTrans_ext line 95
  15. theorem OAI.Problem340.SingularUniversalOperator.identityGenerator_operator line 109
  16. theorem OAI.Problem340.SingularUniversalOperator.natTrans_ext_apply line 115
  17. theorem OAI.Problem340.SingularUniversalOperator.operator_unique line 124