OAI/Geometry/SingularHomology/SingularCoverChains.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.SingularCover.supported line 17
  2. theorem OAI.Problem340.SingularCover.mem_supported line 22
  3. theorem OAI.Problem340.SingularCover.supported_mono line 27
  4. theorem OAI.Problem340.SingularCover.supported_inter line 30
  5. theorem OAI.Problem340.SingularCover.supported_univ line 35
  6. instance OAI.Problem340.SingularCover.chainFunctor_preservesColimitsOfShape line 39
  7. theorem OAI.Problem340.SingularCover.union_isPushout line 49
  8. theorem OAI.Problem340.SingularCover.chainUnion_isPushout line 58
  9. def OAI.Problem340.SingularCover.unionShortComplex line 71
  10. theorem OAI.Problem340.SingularCover.unionShortComplex_exact line 75
  11. theorem OAI.Problem340.SingularCover.chainMap_mono line 79
  12. theorem OAI.Problem340.SingularCover.unionShortComplex_shortExact line 86