OAI/Algebra/FinitisticAsymmetry/Derived/BoundedGeneration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.DerivedSupport.eventuallyIsoCoconeIsColimit line 19
2. def OAI.LittleFinitistic.DerivedSupport.cutSequenceMap line 44
3. def OAI.LittleFinitistic.DerivedSupport.cutSequenceCocone line 47
4. def OAI.LittleFinitistic.DerivedSupport.cutSequenceIsColimit line 53
5. lemma OAI.LittleFinitistic.DerivedSupport.cut_isZero_of_upperBound line 70
6. lemma OAI.LittleFinitistic.DerivedSupport.prop_cut_of_terms line 84
7. lemma OAI.LittleFinitistic.DerivedSupport.prop_single_of_zero line 118
8. lemma OAI.LittleFinitistic.DerivedSupport.prop_of_boundedAbove_terms line 126