OAI/Geometry/SingularHomology/TetrahedronSingular.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.SimplicialSphere.TopologicalBoundary line 13
  2. def OAI.Problem340.SimplicialSphere.tetraVector line 16
  3. lemma OAI.Problem340.SimplicialSphere.tetraVector_ne_zero line 19
  4. lemma OAI.Problem340.SimplicialSphere.continuous_tetraVector line 40
  5. def OAI.Problem340.SimplicialSphere.radial line 52
  6. lemma OAI.Problem340.SimplicialSphere.continuous_radial line 58
  7. def OAI.Problem340.SimplicialSphere.radialMap line 63
  8. lemma OAI.Problem340.SimplicialSphere.map_mem_boundary line 65
  9. def OAI.Problem340.SimplicialSphere.simplexBoundaryMap line 79
  10. lemma OAI.Problem340.SimplicialSphere.simplexBoundaryMap_naturality line 84
  11. lemma OAI.Problem340.SimplicialSphere.radialMap_naturality line 94
  12. def OAI.Problem340.SimplicialSphere.singularSimplex line 103
  13. lemma OAI.Problem340.SimplicialSphere.singularSimplex_naturality line 108
  14. def OAI.Problem340.SimplicialSphere.toSingular line 118
  15. abbrev OAI.Problem340.SimplicialSphere.singularChains line 125
  16. def OAI.Problem340.SimplicialSphere.singularChainMap line 129
  17. def OAI.Problem340.SimplicialSphere.singularFundamentalCycle line 132
  18. lemma OAI.Problem340.SimplicialSphere.singularFundamentalCycle_boundary line 135
  19. def OAI.Problem340.SimplicialSphere.singularFundamentalClassMap line 140
  20. def OAI.Problem340.SimplicialSphere.singularFundamentalClass line 144
  21. theorem OAI.Problem340.SimplicialSphere.singularFundamentalClass_eq_zero_iff line 147