Commit 2021-07-20 07:56 0f58e131

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.