OAI/Topology/ArtinGroups/Harmonic/LateDelay.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.LateDelay line 14
2. def OAI.HarmonicArtin.lateDelayTime line 16
3. lemma OAI.HarmonicArtin.extension_stationary line 35
4. def OAI.HarmonicArtin.extensionEarly line 38
5. def OAI.HarmonicArtin.extensionLate line 41
6. lemma OAI.HarmonicArtin.extension_agree line 44
7. def OAI.HarmonicArtin.extensionValue line 55
8. lemma OAI.HarmonicArtin.extensionValue_early line 59
9. lemma OAI.HarmonicArtin.extensionValue_late line 63
10. lemma OAI.HarmonicArtin.extensionValue_continuous line 74
11. def OAI.HarmonicArtin.extendContraction line 92
12. lemma OAI.HarmonicArtin.extendContraction_old line 111