OAI/Geometry/SingularHomology/TetrahedronChainInjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem340.SimplicialSphere.eq_of_tetraVector_eq_pos_smul line 12
  2. theorem OAI.Problem340.SimplicialSphere.radial_injective line 42
  3. lemma OAI.Problem340.SimplicialSphere.radial_simplexBoundaryMap_injective line 55
  4. theorem OAI.Problem340.SimplicialSphere.singularSimplex_injective line 70
  5. instance OAI.Problem340.SimplicialSphere.toSingular_app_mono line 77
  6. instance OAI.Problem340.SimplicialSphere.toSingular_mono line 81
  7. abbrev OAI.Problem340.SimplicialSphere.singularTetrahedron line 86
  8. def OAI.Problem340.SimplicialSphere.isoSingularTetrahedron line 89
  9. instance OAI.Problem340.SimplicialSphere.toSingular_chainMap_f_mono line 92
  10. instance OAI.Problem340.SimplicialSphere.singularChainMap_f_mono line 97
  11. theorem OAI.Problem340.SimplicialSphere.singularChainMap_f_injective line 104
  12. theorem OAI.Problem340.SimplicialSphere.singularFundamentalCycle_ne_zero line 108
  13. theorem OAI.Problem340.SimplicialSphere.singularFundamentalCycle_one_ne_zero line 114