feat(topology/bases): Topological basis of a product. (#7753)
Given a family of topological spaces `X_i` with topological bases `T_i`, this constructs the associated basis of the product topology.
This also includes a construction of the tautological topological basis consisting of all open sets.
This generalizes a lemma from LTE.
