Add Real TVS trait to Weak topology on separable Hilbert space

[GeoffreySangston]

I just changed 'Has a group topology' to 'Has a real TVS topology' and removed the 'Contractible' trait, which wasn't adding much. There are multiple redundant traits. I don't see a reason to remove them since they have references, but we can if someone wants to.

[prabau]

Looking at why P43 (locally injectively path connected) can now be derived. It relies on the space being Hausdorff.

[TVS => P43] is not known in pi-base, but wouldn't it be true in general, even for non-Hausdorff TVS?

A straight line path between two vectors is continuous. And given a point $x$, any nbhd of $x$ contains an open balanced nbhd $V$. From there, between any two points $y,z\in V$, the nbhd $V$ either contains the line segment between $y$ and $z$ or contains two line segments, from $y$ to $x$ and from $z$ to $x$. etc.

[prabau]

I'll append this comment to #1743 and discuss further over there.