Fix namespace

leanprover-community · Oct 31, 2024 · 3fddedf · 3fddedf
1 parent 0550ad8
commit 3fddedf
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Preserves/Presheaf.lean
@@ -43,6 +43,8 @@ open CategoryTheory Limits
 
 universe v u
 
+namespace CategoryTheory.Limits
+
 section LargeCategory
 
 variable {C : Type u} [Category.{v} C] [HasFiniteColimits C] (A : Cᵒᵖ ⥤ Type v)
@@ -64,8 +66,6 @@ end LargeCategory
 
 variable {C : Type u} [SmallCategory C] [HasFiniteColimits C]
 
-namespace CategoryTheory.Limits
-
 variable (A : Cᵒᵖ ⥤ Type u)
 
 namespace PreservesFiniteLimitsOfIsFilteredCostructuredArrowYonedaAux