normed group todo

Stream: condensed mathematics

[Johan Commelin]

Here's a standalone bit that needs to be done: https://leanprover-community.github.io/liquid/sect0010.html#normed-to-cond
Every normed group $V$ is a topological group, hence condensed: $V(S)$ is the collection of continuous maps $S → V$.
But there is another description of this condensed abelian group: $V(S)$ is also the completion of the group of locally constant maps $S → V$, for the sup-norm.
We need to know that the two points of view are equivalent.