OAI/Algebra/FinitisticAsymmetry/Triangular/Generation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.CummingsConstruction.periodicOld_d line 18
2. def OAI.LittleFinitistic.CummingsConstruction.oldSingleι line 25
3. def OAI.LittleFinitistic.CummingsConstruction.oldSingleπ line 29
4. lemma OAI.LittleFinitistic.CummingsConstruction.oldSingleι_π line 33
5. abbrev OAI.LittleFinitistic.CummingsConstruction.extendedInjective line 39
6. abbrev OAI.LittleFinitistic.CummingsConstruction.extendedRegular line 40
7. abbrev OAI.LittleFinitistic.CummingsConstruction.extendedOld line 41
8. def OAI.LittleFinitistic.CummingsConstruction.regularDerivedIso line 45
9. def OAI.LittleFinitistic.CummingsConstruction.oldSingleDerivedIso line 51
10. lemma OAI.LittleFinitistic.CummingsConstruction.extended_shortExact line 59
11. lemma OAI.LittleFinitistic.CummingsConstruction.extendedInjective_mem line 72
12. lemma OAI.LittleFinitistic.CummingsConstruction.oldSimple_shifted_retract line 84
13. lemma OAI.LittleFinitistic.CummingsConstruction.oldSimple_mem line 110
14. lemma OAI.LittleFinitistic.CummingsConstruction.newRegular_mem line 116
15. lemma OAI.LittleFinitistic.CummingsConstruction.newSimple_mem line 121
16. lemma OAI.LittleFinitistic.CummingsConstruction.injectivesGenerate line 138