OAI/GroupTheory/FiniteType/BasedHorn.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BasedHorn.face_compatible line 27
  2. def OAI.BasedHorn.fill line 38
  3. lemma OAI.BasedHorn.fill_face line 41
  4. lemma OAI.BasedHorn.fill_doubleBoundary line 45
  5. lemma OAI.BasedHorn.lastFace_injective line 60
  6. def OAI.BasedHorn.pairFaces line 67
  7. def OAI.BasedHorn.pairFill line 71
  8. lemma OAI.BasedHorn.pairFill_doubleBoundary line 74
  9. lemma OAI.BasedHorn.pairFill_early line 77
  10. lemma OAI.BasedHorn.pairFill_left line 89
  11. lemma OAI.BasedHorn.pairFill_right line 96
  12. def OAI.BasedHorn.product line 104
  13. lemma OAI.BasedHorn.product_class line 107
  14. lemma OAI.HurewiczAddition.alternating_cycle_boundary line 119
  15. lemma OAI.HurewiczAddition.cycleClassHom_sum line 129
  16. lemma OAI.HurewiczAddition.alternating_class_zero line 144
  17. lemma OAI.HurewiczAddition.homologyClass_const line 156
  18. lemma OAI.HurewiczAddition.alternating_three line 167
  19. lemma OAI.HurewiczAddition.homologyClass_product line 182
  20. lemma OAI.DuffyHurewicz.homologyClass_homotopic line 210
  21. def OAI.DuffyHurewicz.value line 215
  22. lemma OAI.DuffyHurewicz.value_class line 224
  23. lemma OAI.DuffyHurewicz.value_mul line 229
  24. def OAI.DuffyHurewicz.hom line 240
  25. lemma OAI.DuffyHurewicz.hom_class line 243
  26. lemma OAI.DuffyHurewicz.range_canonical_le_range line 246
  27. theorem OAI.DuffyHurewicz.surjective line 258