Commit 2020-05-13 03:44 4857284a

feat(topology/bounded_continuous_function): the normed space C^0 (#2660) For β a normed (vector) space over a nondiscrete normed field 𝕜, we construct the normed 𝕜-space structure on the set of bounded continuous functions from a topological space into β.