Topology lemmas

[Brixfoly]

Motivation for this change

fyi @affeldt-aist @hoheinzollern @mkerjean
The goal of this PR is to add the topological notion of separability (which is useful for the implementation of the Bochner Integral I was doing, but it is useful for a lot of other stuff), with some lemmas alongside it. It also contains a lemma basisP that states the equivalence between the definition of a topological basis with neighbourhoods and the one with open sets.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[Brixfoly]

A bit broken because it is on top of pr 2008 (but can be made independent from it)

[Brixfoly]

Shouldn't have added anything past commit dc44e76

[affeldt-aist]

@Brixfoly can you try to rebase? I forgot what it was about :-(

[affeldt-aist]

@Brixfoly can you try to rebase? I forgot what it was about :-(

ping

[Brixfoly]

Ok the merge is wrong I should have checked, I will do another version

[Brixfoly]

@affeldt-aist It should be good to go now, I've cleaned up some proof, tell me if the lemmas look ok to you

[affeldt-aist]

@t6s you might want to take a look at this PR (it is about basis, should be treated soon)

[t6s]

The contents look nice. The code would only need some minor cleaning so that it would follow the style guide (spacing and indentation). I would also suggest documenting the intention in the PR comment (currently a one-liner "fyi ...").

[Brixfoly]

I have made an update of this (rebase+name clean-up following your recommendations), but I still need to push it