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.

source

theorem TopCat.isTopologicalBasis_cofiltered_limit {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] (F : CategoryTheory.Functor J TopCatMax) (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 : Set ↑(F.obj j)), V ∈ T j → ↑(F.map f) ⁻¹' V ∈ T i) :

TopologicalSpace.IsTopologicalBasis {U | ∃ j V, V ∈ T j ∧ U = ↑(C.π.app j) ⁻¹' V}