OAI/GroupTheory/FiniteType/RelativeChainsEmptyProjectionQuasiIso.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RelativeChains.empty_projection_quasiIso line 14
  2. def OAI.RelativeChains.twoPointHomologyIso line 17
  3. lemma OAI.SphereCover.val_ne_zero line 40
  4. lemma OAI.SphereCover.eq_or_neg_of_finrank_one line 47
  5. lemma OAI.SphereCover.finite_of_finrank_one line 59
  6. def OAI.SphereCover.baseHomologyIso line 67
  7. lemma OAI.SphereCover.baseHomology_isZero line 73
  8. theorem OAI.SphereCover.homology line 84
  9. lemma OAI.SphereCover.normed_homology line 126
  10. def OAI.RelativeChains.contractiblePairIso line 145
  11. lemma OAI.RelativeChains.contractiblePair_zero line 152
  12. abbrev OAI.DiskHomology.Disk line 162
  13. abbrev OAI.DiskHomology.Boundary line 163
  14. def OAI.DiskHomology.boundaryEquiv line 165
  15. lemma OAI.DiskHomology.contractible line 174
  16. lemma OAI.DiskHomology.homology line 177
  17. abbrev OAI.FinsuppHomology.obj line 202
  18. def OAI.FinsuppHomology.map line 203
  19. lemma OAI.FinsuppHomology.map_apply line 205
  20. def OAI.FinsuppHomology.singleObj line 208
  21. def OAI.FinsuppHomology.sumMap line 210
  22. lemma OAI.FinsuppHomology.sumMap_single line 212
  23. def OAI.FinsuppHomology.complex line 215
  24. def OAI.FinsuppHomology.single line 236
  25. def OAI.FinsuppHomology.eval line 245
  26. lemma OAI.FinsuppHomology.single_eval line 249
  27. lemma OAI.FinsuppHomology.single_eval_ne line 253
  28. def OAI.FinsuppHomology.homologySum line 259
  29. lemma OAI.FinsuppHomology.homologySum_single line 263
  30. lemma OAI.FinsuppHomology.eval_homologySum line 268
  31. lemma OAI.FinsuppHomology.homologySum_injective line 282
  32. lemma OAI.FinsuppHomology.homologySum_surjective line 291
  33. def OAI.FinsuppHomology.homologyIso line 325