OAI/Algebra/FinitisticAsymmetry/Derived/LocalizingRetracts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.DerivedSupport.swindleA line 15
2. def OAI.LittleFinitistic.DerivedSupport.swindleC line 18
3. def OAI.LittleFinitistic.DerivedSupport.swindleB line 23
4. def OAI.LittleFinitistic.DerivedSupport.swindleI line 27
5. lemma OAI.LittleFinitistic.DerivedSupport.swindleAC line 31
6. lemma OAI.LittleFinitistic.DerivedSupport.swindleAB line 40
7. lemma OAI.LittleFinitistic.DerivedSupport.swindleIB line 46
8. lemma OAI.LittleFinitistic.DerivedSupport.swindleIC line 49
9. lemma OAI.LittleFinitistic.DerivedSupport.swindleTotal line 52
10. def OAI.LittleFinitistic.DerivedSupport.swindleIso line 64
11. lemma OAI.LittleFinitistic.DerivedSupport.swindle_distinguished line 72
12. lemma OAI.LittleFinitistic.DerivedSupport.localizing_of_retract line 84