pushforward of product topology is product topology

Stream: Is there code for X?

[Kevin Buzzard]

Do we have anything like

import Mathlib.Topology.Constructions

example {ι κ : Type*} (e : ι ≃ κ) (X : Type*) [TopologicalSpace X] :
    TopologicalSpace.coinduced (fun f ↦ f ∘ e : (κ → X) → (ι → X)) Pi.topologicalSpace =
    Pi.topologicalSpace := by
  sorry

Mathematically I'm asking that the product topologies on $X^m$ and $X^n$ coincide given a bijection $m=n$. The map (κ → X) → (ι → X) can be beefed up to can equiv with Equiv.piCongrLeft' if necessary. I tried doing this with some lattice manipulations but didn't get anywhere, and breaking it up into <= and >= didn't look like much fun either.

[Yury G. Kudryashov]

We have docs#Homeomorph.piCongrLeft

[Kevin Buzzard]

Perfect, thanks!