Equivalence between pi type over singleton and type

Stream: Is there code for X?

[Rémy Degenne]

Do we have something like the following?

import Mathlib.Topology.Homeomorph

example {ι : Type*} (α : ι → Type*) [∀ i, TopologicalSpace (α i)] (i : ι) :
    (Π j : ({i} : Set ι), α j) ≃ₜ α i := sorry

[Eric Wieser]

I would expect it to be stated for Unique rather than a singleton

[Daniel Weber]

Is this docs#Homeomorph.funUnique ?

[Daniel Weber]

Ah, no, that's nondependent

[Daniel Weber]

example {ι : Type*} [Unique ι] (α : ι → Type*) [∀ i, TopologicalSpace (α i)] : (Π j, α j) ≃ₜ α default where
  toEquiv := Equiv.piUnique α
  continuous_toFun := continuous_apply _
  continuous_invFun := continuous_pi fun x => by
    cases x using uniqueElim
    exact continuous_id

[Eric Wieser]

I think the non-dependent one should just be an abbrev for what you wrote there

[Rémy Degenne]

Thanks! That works perfectly!

[Rémy Degenne]

Do you want to PR it? If not, I'll do it at some point when PRing my code that needs it.