C(S, V) complete and separated

Stream: Is there code for X?

[Johan Commelin]

If V is a complete/separated uniform space, do we know that the space of continuous maps C(S, V) is also complete/separated?

We need this for LTE.

[Yaël Dillies]

docs#continuous_map.complete_space. I can't find the separated_space instance.

[Yaël Dillies]

It is also not quite in the generality you ask for.

[Johan Commelin]

Ooh, but that one should be good enough for my purposes. I wonder why I missed it

[Yaël Dillies]

yael_search always here to serve!

[Anatole Dedecker]

Separation is docs#continuous_map.t2_space

[Yaël Dillies]

What is the difference between separated_space and t2_space?

[Anatole Dedecker]

If anyone is hungry for refactors (looking at you Yaël) I think we want to throw away docs#separated_space

[Anatole Dedecker]

The only difference is that one is expressed about uniformities, but really it should just be a lemma saying « the topology associated to this uniformity is T2 iff […] »