Zulip Chat Archive

Stream: maths

Topic: continuous functions into a topological X form an X


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

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 (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: Dec 20 2023 at 11:08 UTC