continuous functions into a topological X form an X

Stream: maths

[Scott Morrison]

Do we already have

instance {α : Type u} {β : Type v} [topological_space α] [topological_space β] [has_mul β] : has_mul (subtype (@continuous α β _ _)) := ...

and all its friends available in mathlib?

[Scott Morrison]

Is there some efficient way to generate them all, if not?

[Patrick Massot]

We don't. We could hope to write a version of subtype_instance/pi_instance to get them, but I'm not sure the lemma naming convention are strong enough here

[Scott Morrison]

I guess it's actually pretty easy. You only have to do any work for has_add and has_mul; all the axioms are free.