Tietze's theorem

[zstone1]

Motivation for this change

In the apparently never-ending results needed for fundamental theorem, here's Tietze's Extension theorem. We're continuing along #965 to show that continuous functions are dense in L1.

A few things to note:

1. Normally, Tietze's theorem assumes X is normal. Here, we assume it has urysohn extensions. Urysohn's lemma (Urysohn's Lemma #900) is the proof that these are equivalent. We could directly show that pseudometric spaces have urysohn extensions, once we get that far if we had to. Or we can merge in the urysohns' lemma PR, move to HB, and just do it that way.
2. Urysohn's lemma has several variants, including a form unbounded functions. The proof is straightforward, by composing f with x/(1+|x|) and applying the bounded version. We don't need it right now, so we can deal with that later.
3. The proof itself is a rather straightforward duplication of the textbook argument. It's about 80% analysis with geometric series. Big thanks to all the posnum stuff automating away several days of work!

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

I re-read the scripts and could find a number of shortcuts that I have committed.
What about using notations such as:
Local Notation "'2/3" := (PosNum twothirds_pos).
in continuous_bounded_extension?
That could make intermediate goals a bit shorter and more readable.
(Yet, inside this proof the problem is not here ^_^.)

[zstone1]

Turns out Local Notation "3" := 3%:R. is good enough to clean up the annoying notational issues. Just using 2/3 infers positivity as expected.