OAI/Algebra/GroupRing/CellHEP.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TorsionFreeZeroDivisors.CellHEP.Cylinder line 14
2. def OAI.TorsionFreeZeroDivisors.CellHEP.denom line 15
3. lemma OAI.TorsionFreeZeroDivisors.CellHEP.denom_pos line 16
4. lemma OAI.TorsionFreeZeroDivisors.CellHEP.denom_le_two line 18
5. def OAI.TorsionFreeZeroDivisors.CellHEP.scale line 21
6. lemma OAI.TorsionFreeZeroDivisors.CellHEP.scale_nonneg line 22
7. lemma OAI.TorsionFreeZeroDivisors.CellHEP.scale_ge_one line 23
8. lemma OAI.TorsionFreeZeroDivisors.CellHEP.scale_time line 26
9. lemma OAI.TorsionFreeZeroDivisors.CellHEP.scale_norm line 31
10. def OAI.TorsionFreeZeroDivisors.CellHEP.retract line 35
11. lemma OAI.TorsionFreeZeroDivisors.CellHEP.continuous_retract line 44
12. def OAI.TorsionFreeZeroDivisors.CellHEP.Rim line 50
13. lemma OAI.TorsionFreeZeroDivisors.CellHEP.retract_mem line 51
14. lemma OAI.TorsionFreeZeroDivisors.CellHEP.retract_eq line 67
15. def OAI.TorsionFreeZeroDivisors.CellHEP.retraction line 84
16. def OAI.TorsionFreeZeroDivisors.CellHEP.face line 87
17. lemma OAI.TorsionFreeZeroDivisors.CellHEP.face_closed line 90
18. lemma OAI.TorsionFreeZeroDivisors.CellHEP.face_cover line 95
19. def OAI.TorsionFreeZeroDivisors.CellHEP.faceMap line 103
20. lemma OAI.TorsionFreeZeroDivisors.CellHEP.faceMap_compat line 111
21. def OAI.TorsionFreeZeroDivisors.CellHEP.rimMap line 124
22. lemma OAI.TorsionFreeZeroDivisors.CellHEP.rimMap_face line 127
23. def OAI.TorsionFreeZeroDivisors.CellHEP.extension line 132

    Source documentation

    Literal homotopy extension for a cell, with no fibrancy premise.

    def extension : C(Cylinder n,Y) := (rimMap f H h).comp retraction

    Mentions: OAI.TorsionFreeZeroDivisors.CellHEP.Cylinder, OAI.TorsionFreeZeroDivisors.CellHEP.rimMap, OAI.TorsionFreeZeroDivisors.CellHEP.retraction

24. lemma OAI.TorsionFreeZeroDivisors.CellHEP.extension_zero line 133
25. lemma OAI.TorsionFreeZeroDivisors.CellHEP.extension_boundary line 138