subspace open map

[zstone1]

Motivation for this change

A simple theorem that the weak topology and the subspace topology are "the same thing". In particular, this is useful for knowing that projT1 is an embedding of {x : T | B x} into subspace B. We'll want this for homotopy theory so we can do topology and paths of {x : T | B x} and do algebra in subspace B.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
  (do not edit former entries, only append new ones, be careful:
  merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

I don't see any problem. I just made a commit to remove shorten a related lemma.