OAI/Algebra/GroupRing/AttachmentHEP.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.eval line 18
2. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.basePaths line 19
3. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.cellPaths line 20
4. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.cellPaths_boundary line 26
5. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.cellPaths_zero line 34
6. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.paths line 38
7. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.paths_base line 40
8. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.paths_zero line 41
9. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.extend line 53

   Source documentation

   Homotopy extension for a genuine disk attachment with arbitrarily many cells. Currying into the compact-open path space respects the weak topology.

   def extend : C(unitInterval × Space a,Y) := (paths a f H h).uncurry.comp ⟨Prod.swap,continuous_swap⟩

   Mentions: OAI.TorsionFreeZeroDivisors.AttachmentHEP.paths

10. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.extend_base line 54
11. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.extend_zero line 55
12. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.endpoint line 56
13. def OAI.TorsionFreeZeroDivisors.AttachmentHEP.homotopy line 57
14. lemma OAI.TorsionFreeZeroDivisors.AttachmentHEP.endpoint_base line 61