[affeldt-aist]

Motivation for this change

This PR extracts the lemma accessible_field from PR #2022,
put it at the level of metric spaces, and for that purpose provides the lemma ball_open at the level of metric spaces.

So far ball_open was available from pseudoMetricNormedZmodType, but it appears
that its uses can be superseded by the new ball_open.

The version available so far is therefore renamed to pseudo_ball_open to mark the difference.

PS: the changes in function_spaces.v shouldn't be here, they are here by accident, but that's just cosmetics

Checklist

• appended entries in the relevant sections of 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 likely to be merged as they are 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

[nmolinamounier]

The type of accessible_space should be generalized.

Side note on the relevant separation axioms, to clarify the full breadth of the result (related to #2156): every metric space is perfectly normal Hausdorff which implies all separation axioms currently implemented, including accessible_space. That said, the codomain of metric/norms probably needs to embed into $$\mathbb{R}$$ for the proof of completely_regular_space to work.