OAI/Algebra/FinitisticAsymmetry/Derived/UpperTruncation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.DerivedSupport.upperSub line 20
  2. lemma OAI.LittleFinitistic.DerivedSupport.mem_upperSub line 23
  3. lemma OAI.LittleFinitistic.DerivedSupport.upperSub_d line 32
  4. def OAI.LittleFinitistic.DerivedSupport.upper line 47
  5. def OAI.LittleFinitistic.DerivedSupport.upperι line 63
  6. lemma OAI.LittleFinitistic.DerivedSupport.upper_le line 67
  7. def OAI.LittleFinitistic.DerivedSupport.upperMap line 78
  8. lemma OAI.LittleFinitistic.DerivedSupport.upperMap_ι line 84
  9. lemma OAI.LittleFinitistic.DerivedSupport.upperι_f_isIso line 87
  10. lemma OAI.LittleFinitistic.DerivedSupport.upper_isZero_X line 92
  11. def OAI.LittleFinitistic.DerivedSupport.upperSequenceMap line 105
  12. def OAI.LittleFinitistic.DerivedSupport.upperSequenceCocone line 108
  13. def OAI.LittleFinitistic.DerivedSupport.upperSequenceIsColimit line 114
  14. lemma OAI.LittleFinitistic.DerivedSupport.prop_of_all_modules line 127
  15. lemma OAI.LittleFinitistic.DerivedSupport.localizing_eq_top_of_all_modules line 134