## Stream: maths

### Topic: continuous functions into a topological X form an X

#### Scott Morrison (Apr 08 2019 at 05:58):

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


and all its friends available in mathlib?

#### Scott Morrison (Apr 08 2019 at 05:58):

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

#### Patrick Massot (Apr 08 2019 at 06:30):

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 (Apr 08 2019 at 06:56):

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.

Last updated: May 06 2021 at 18:20 UTC