PiLp complete space?

Stream: maths

[Robert Maxton]

• Is it in fact true that PiLp takes a collection of complete spaces to a complete space in general/for 'most' values of p? I would be quite surprised to find out that e.g. normal Euclidean space is not complete, but I have been quite surprised before, and there is a somewhat suspicious pattern of instances for very specific cases.
• If it is true, what's the easiest way to show it?
• Alternatively, maybe we should open a discussion about just changing the p used in docs#Topology.RelCWComplex and the p used in docs#TopCat.RelativeCWComplex to be the same....

[Jireh Loreaux]

It's complete. The uniformity on PiLp is precisely the uniformity on the pi type.

[Jireh Loreaux]

It looks like we have written it for Prod here docs#WithLp.instProdCompleteSpace but not for Pi

[Robert Maxton]

Good to know. I ended up working around it, but might put some time towards building a general instance then.

[Jireh Loreaux]

I'm saying it's trivial to build the CompleteSpace instance. It's just inferInstanceAs ...

[Robert Maxton]

Oh, well. That's helpful. I'll definitely PR a copy for Pi then

[Robert Maxton]

Thanks!