mathlib3

16157f26 - chore(topology/continuous_function/bounded): generalize from `normed_*` to `semi_normed_*` (#13915)

chore(topology/continuous_function/bounded): generalize from `normed_*` to `semi_normed_*` (#13915) Every single lemma in this file generalized, apart from the ones that transferred a `normed_*` instance which obviously need the stronger assumption. `dist_zero_of_empty` was the only lemma that actually needed reproving from scratch, all the other affected proofs are just split between two instances.