Zulip Chat Archive

Stream: maths

Topic: continuous functions into a topological X form an X


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Apr 08 2019 at 05:58):

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

view this post on Zulip 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

view this post on Zulip 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