theorem TopCat.Sheaf.filteredColimit_presheaf_isSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {X : TopCat} {J : Type t} [CategoryTheory.Category.{t, t} J] [CategoryTheory.IsFiltered J] [TopologicalSpace.NoetherianSpace ↑X] [CategoryTheory.Limits.HasColimitsOfShape J C] (F : CategoryTheory.Functor J (Sheaf C X)) (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.sheafToPresheaf (Opens.grothendieckTopology ↑X) C))) (hc : CategoryTheory.Limits.IsColimit c) : Presheaf.IsSheaf c.pt

Lem 22, Lec 12: on a Noetherian space, a filtered colimit of sheaves is already a sheaf; equivalently, the underlying presheaf colimit satisfies the sheaf condition because finite covers and filtered colimits commute.