Commit 2022-05-03 18:19 16157f26
View on Github →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.