fix a name

dagurtomas · Jun 14, 2024 · 67ad313 · 67ad313
1 parent 73700ed
commit 67ad313
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/LeanCondensed/Projects/AB.lean b/LeanCondensed/Projects/AB.lean
@@ -152,8 +152,7 @@ lemma abStar_iff_preserves_epi [HasLimitsOfShape I A] :
     have := h F hh
     exact this.epi_g
 
--- Stating and proving the converse of this lemma should be easy
-lemma ab_of_preserves_mono [HasColimitsOfShape I A] :
+lemma ab_iff_preserves_mono [HasColimitsOfShape I A] :
     ((∀ (F : I ⥤ ShortComplex A),
     (∀ i, (F.obj i).ShortExact) → Mono (ShortComplex.colimitCocone F).pt.f)) ↔
       HasExactColimitsOfShape I A := by