nbhs basis in tvs.v

[mkerjean]

In the axioms of a convexTvs, locally_convex should assume the convexity of a basis of 0-neighbourhoods, not of a basis of open sets.

  locally_convex : exists2 B : set_system E,
    (forall b, b \in B -> convex_set b) & basis B

should be

  locally_convex : exists2 B : set_system E,
    (forall b, b \in B -> convex_set b) &  filter_from [set U | B U /\ U 0] id --> 0.

[mkerjean]

This issue is corrected within PR#1963, I will do an indenpendant PR to solve this issue only.