OAI/GroupTheory/FiniteType/HurewiczInverse.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HurewiczInverse.coherent line 29
  2. lemma OAI.HurewiczInverse.coherent_top line 34
  3. lemma OAI.HurewiczInverse.coherent_fixed line 39
  4. def OAI.HurewiczInverse.normalize line 43
  5. lemma OAI.HurewiczInverse.normalize_const line 51
  6. lemma OAI.HurewiczInverse.hom_relative line 58
  7. lemma OAI.HurewiczInverse.normalize_class line 73
  8. lemma OAI.HurewiczInverse.top_double line 77
  9. lemma OAI.HurewiczInverse.top_basedFace line 91
  10. abbrev OAI.HurewiczInverse.A line 97
  11. def OAI.HurewiczInverse.chainValue line 99
  12. lemma OAI.HurewiczInverse.generator_chainValue line 102
  13. lemma OAI.HurewiczInverse.boundary_chainValue line 107
  14. def OAI.HurewiczInverse.inverse line 118
  15. lemma OAI.HurewiczInverse.homologyπ_inverse line 130
  16. lemma OAI.HurewiczInverse.cycleClassHom_inverse line 134
  17. lemma OAI.HurewiczInverse.inverse_homologyClass line 147
  18. lemma OAI.HurewiczInverse.leftInverse line 154
  19. theorem OAI.DuffyHurewicz.injective line 170
  20. theorem OAI.DuffyHurewicz.bijective line 175
  21. theorem OAI.HurewiczConstruction.exists_sphere line 187
  22. def OAI.HurewiczConstruction.actionMap line 211
  23. lemma OAI.HurewiczConstruction.actionMap_one line 213
  24. lemma OAI.HurewiczConstruction.actionMap_mul line 214
  25. def OAI.HurewiczConstruction.homologyRep line 217
  26. abbrev OAI.HurewiczConstruction.homologyModule line 225
  27. def OAI.HurewiczConstruction.sphereModuleClass line 227
  28. theorem OAI.HurewiczConstruction.finite_sphere_generators line 231
  29. lemma OAI.HurewiczConstruction.homotopy_zero line 250
  30. lemma OAI.HurewiczConstruction.homotopy_one line 254
  31. theorem OAI.HurewiczConstruction.homotopy_trivial_of_homology_zero line 258
  32. lemma OAI.HurewiczConstruction.homology_zero_of_homotopy line 278