Homeomorph.curry

Stream: mathlib4

[Vasilii Nesterov]

In #26149 I proved

def Homeomorph.curry {X Y Z : Type*} [TopologicalSpace Z] : (X × Y → Z) ≃ₜ (X → Y → Z)

but found that we already have

def Homeomorph.curry {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    [LocallyCompactSpace X] [LocallyCompactSpace Y] :
    C(X × Y, Z) ≃ₜ C(X, C(Y, Z))

Which one should be called curry?

[Patrick Massot]

Your statement looks too specialized to get this name, so I would search another name for it, clearly mentioning the product topology.

[Aaron Liu]

Patrick Massot said:

Your statement looks too specialized to get this name, so I would search another name for it, clearly mentioning the product topology.

What do you mean by this?

[Jireh Loreaux]

Patrick's point is that the topology on X × Y → Z is the product topology (or, in Lean parlance, docs#Pi.topologicalSpace), and likewise for X → Y → Z.

[Aaron Liu]

oh yeah that's yeah ok

[Aaron Liu]

I thought Patrick was referring to the binary product