OAI/GroupTheory/FiniteType/CWCellularSkelInclHomologyIsIso.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CWCellular.skelIncl_homology_isIso line 16
  2. lemma OAI.CWCellular.skelLE_homology_isIso line 27
  3. lemma OAI.CWCellular.toComplex_injective line 41
  4. lemma OAI.CWCellular.toComplex_comp line 53
  5. lemma OAI.CWCellular.chain_lift line 59
  6. lemma OAI.CWCellular.chain_lift_above line 90
  7. lemma OAI.CWCellular.chain_homologyMap_class line 99
  8. lemma OAI.CWCellular.homology_toComplex_surjective line 106
  9. lemma OAI.CWCellular.homology_toComplex_injective line 134
  10. lemma OAI.CWCellular.homology_toComplex_isIso line 161
  11. lemma OAI.CWCellular.skelIncl_homology_epi line 174
  12. lemma OAI.CWCellular.skelLE_homology_epi line 180
  13. lemma OAI.CWCellular.homology_toComplex_surjective_top line 194
  14. def OAI.CWCellular.skeletonHomeo line 231
  15. lemma OAI.CWCellular.skeleton_factor line 234
  16. lemma OAI.CWCellular.homology_skeleton_surjective line 238
  17. lemma OAI.CWCellular.homology_skeleton_bijective line 255