mathlib

4857284a - feat(topology/bounded_continuous_function): the normed space C^0 (#2660)

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 β.