fix(Condensed): remove unnecessary Precoherent assumption (#9730)

leanprover-community · Jan 14, 2024 · 21a2343 · 21a2343
1 parent 7bffe36
commit 21a2343
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Condensed/Explicit.lean b/Mathlib/Condensed/Explicit.lean
@@ -34,7 +34,7 @@ open CategoryTheory Limits Opposite Functor Presieve regularCoverage
 namespace CategoryTheory
 
 variable {C : Type u} [Category.{v} C] (F : Cᵒᵖ ⥤ Type (max u v)) [Preregular C]
-  [FinitaryPreExtensive C] [Precoherent C]
+  [FinitaryPreExtensive C]
 
 theorem isSheaf_coherent_iff_regular_and_extensive : IsSheaf (coherentTopology C) F ↔
     IsSheaf (extensiveCoverage C).toGrothendieck F ∧