Renaming weak topology as initial topology

[mkerjean]

Should weak_topology as described in weak_topology.v be renamed to initial_topology ?

In my opinion, "weak topology" is more often used to refer to the weak topology induced on a E : normedtype or a E: tvstype by its dual E'.

I'm afraid this terminology might lead to confusion for several new users. It has for me, but it might be specific to the mathematics I've learned, so I would value different opinions. What do you think @zstone1 @CohenCyril ?

[CohenCyril]

yes

[CohenCyril]

According to at least https://en.m.wikipedia.org/wiki/Initial_topology you are obviously right @mkerjean