continuity of multiple argument function

Stream: general

[Bernd Losert]

Say I have a function f : a -> a -> a -> a where a is a topological space. How do you prove that it is continuous? Do I have to uncurry it and prove that the uncurried version is continuous on the product space? Given that the category of topological spaces is not cartesian closed, I can't always do this.

[Oliver Nash]

I suspect you probably want to talk about continuity of the uncurried function.

[Oliver Nash]

Recall that a function f : α → β → γ (for types α, β, γ) is really a function from α to the type of functions β → γ.

[Oliver Nash]

Spaces of functions do carry natural topologies and in the locally compact case, the two possible notions will agree. Furthermore Mathlib knows this see: docs#homeomorph.curry

[Bernd Losert]

I will work in the more general setting of convergence spaces, so I won't need to deal with local compactness. But thanks for that link. That helps. Are you familiar with how mathlib proves continuity of group operations in the case of topological groups?

[Oliver Nash]

Are you familiar with how mathlib proves continuity of group operations in the case of topological groups?

I'm not sure you really mean to ask this question. The proof of continuity of group operations depends on the group so there is no single answer to how Mathlib does this.

[Oliver Nash]

I suspect you may mean to ask how Mathlib defines topological groups. For this see docs#topological_group

[Alexander Bentkamp]

There are two options to express continuity of a function with two (or more) arguments. Either you use the product space:
https://leanprover-community.github.io/mathlib_docs/topology/algebra/monoid.html#continuous_mul
Or you use continuous maps from another arbitrary space:
https://leanprover-community.github.io/mathlib_docs/topology/algebra/monoid.html#continuous.mul
Maybe this latter option is what you are looking for?

[Bernd Losert]

Aha, so has_continuous_mul is basically doing it on the product space. I see. That's what I was looking for.

[Bernd Losert]

So I guess I can't avoid the curry/uncurry friction.

[Alexander Bentkamp]

Well, you can formulate it as in docs#continuous.mul. That avoids the uncurrying.

[Bernd Losert]

Alright. Thanks a lot.