OAI/Geometry/SingularHomology/SingularSmallNaturality.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SingularSmallChains.singularFunctor line 11
  2. abbrev OAI.Problem340.SingularSmallChains.singularDegree line 15
  3. def OAI.Problem340.SingularSmallChains.memberInclusion line 21
  4. theorem OAI.Problem340.SingularSmallChains.memberInclusion_inclusion line 26
  5. def OAI.Problem340.SingularSmallChains.simplexMember line 33
  6. theorem OAI.Problem340.SingularSmallChains.simplexMember_property line 36
  7. def OAI.Problem340.SingularSmallChains.simplexInMember line 41
  8. theorem OAI.Problem340.SingularSmallChains.simplexInMember_map line 46
  9. def OAI.Problem340.SingularSmallChains.restrict line 55
  10. theorem OAI.Problem340.SingularSmallChains.generator_restrict line 62
  11. theorem OAI.Problem340.SingularSmallChains.restrict_inclusion line 70
  12. theorem OAI.Problem340.SingularSmallChains.restrict_id line 93
  13. theorem OAI.Problem340.SingularSmallChains.restrict_zero line 100
  14. theorem OAI.Problem340.SingularSmallChains.restrict_add line 106
  15. theorem OAI.Problem340.SingularSmallChains.restrict_comp line 113
  16. def OAI.Problem340.SingularSmallChains.restrictChainMap line 120
  17. theorem OAI.Problem340.SingularSmallChains.restrictChainMap_inclusion line 133
  18. theorem OAI.Problem340.SingularSmallChains.restrictChainMap_id line 139
  19. theorem OAI.Problem340.SingularSmallChains.restrictChainMap_comp line 144
  20. def OAI.Problem340.SingularSmallChains.HomotopyNatural line 151
  21. def OAI.Problem340.SingularSmallChains.homotopyOperator line 157
  22. def OAI.Problem340.SingularSmallChains.restrictHomotopy line 163
  23. theorem OAI.Problem340.SingularSmallChains.restrictHomotopy_inclusion line 203