mathlib

0f58e131 - chore(topology/continuous_function, analysis/normed_space): use `is_empty α` instead of `¬nonempty α` (#8352)

chore(topology/continuous_function, analysis/normed_space): use `is_empty α` instead of `¬nonempty α` (#8352) Two lemmas with their assumptions changed, and some proofs golfed using the new forms of these and other lemmas.