Commit 2022-05-03 18:19 16157f26

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.