Commit 2021-06-02 04:57 6c912dec
View on Github →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.