∀ {ι : Type u_5} {X : ι → Type u_9} {g : (a : ι) → Set (Set (X a))} [Finite ι],
  (∀ (a : ι), ⋃₀ g a = Set.univ) →
    Pi.topologicalSpace = TopologicalSpace.generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = Set.univ.pi s}