Commit 2026-05-04 20:38 6b3db580
View on Github →feat(Mathlib/Topology): functional-analytic prereqs for PR 37984 (#38701)
Various miscellaneous constructions around spaces of continuous functions and continuous linear maps, needed for the theory of nonarchimedean measures being developed in PR 37984. The main new result is a criterion for the map
C(X, R) ⊗[R] C(Y, R) → C(X × Y, R) to have dense image.