OAI/Algebra/FinitisticAsymmetry/Derived/Truncations.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.DerivedSupport.cutSub line 16
2. lemma OAI.LittleFinitistic.DerivedSupport.mem_cutSub line 19
3. lemma OAI.LittleFinitistic.DerivedSupport.cutSub_d line 23
4. def OAI.LittleFinitistic.DerivedSupport.cut line 34
5. def OAI.LittleFinitistic.DerivedSupport.cutι line 50
6. instance OAI.LittleFinitistic.DerivedSupport.cutι_mono line 54
7. lemma OAI.LittleFinitistic.DerivedSupport.cutSub_le line 59
8. def OAI.LittleFinitistic.DerivedSupport.cutMap line 65
9. lemma OAI.LittleFinitistic.DerivedSupport.cutMap_ι line 71
10. lemma OAI.LittleFinitistic.DerivedSupport.cut_isZero_X line 74
11. lemma OAI.LittleFinitistic.DerivedSupport.cutι_f_isIso line 82
12. def OAI.LittleFinitistic.DerivedSupport.cutπ line 88
13. lemma OAI.LittleFinitistic.DerivedSupport.cutMap_π line 94
14. instance OAI.LittleFinitistic.DerivedSupport.cutMap_mono line 99
15. instance OAI.LittleFinitistic.DerivedSupport.cutπ_f_self_isIso line 106
16. instance OAI.LittleFinitistic.DerivedSupport.cutπ_epi line 113
17. def OAI.LittleFinitistic.DerivedSupport.cutShortComplex line 120
18. lemma OAI.LittleFinitistic.DerivedSupport.cut_shortExact line 124