Cofiltered limits in the category of topological spaces

Given a compatible collection of topological bases for the factors in a cofiltered limit which contain Set.univ and are closed under intersections, the induced naive collection of sets in the limit is, in fact, a topological basis.

theorem TopCat.isTopologicalBasis_cofiltered_limit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] (F : CategoryTheory.Functor J TopCat) (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C) (T : (j : J) → Set (Set ↑(F.obj j))) (hT : ∀ (j : J), TopologicalSpace.IsTopologicalBasis (T j)) (univ : ∀ (i : J), Set.univ ∈ T i) (inter : ∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i) (compat : ∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(F.map f) ⁻¹' V ∈ T i) : TopologicalSpace.IsTopologicalBasis {U : Set ↑C.pt | ∃ (j : J), ∃ V ∈ T j, U = ⇑(C.π.app j) ⁻¹' V}

Given a compatible collection of topological bases for the factors in a cofiltered limit which contain Set.univ and are closed under intersections, the induced naive collection of sets in the limit is, in fact, a topological basis.