∀ {Y : Type v} {ι : Type u_5} [inst : TopologicalSpace Y] {ι' : Type u_9} (φ : ι' → ι),
  TopologicalSpace.induced (fun x => x ∘ φ) Pi.topologicalSpace =
    ⨅ i', TopologicalSpace.induced (Function.eval (φ i')) inst