Commit 2021-03-27 03:05 832a2eb9

refactor(topology/continuous_functions): change file layout (#6890) Moves topology/bounded_continuous_function.lean to topology/continuous_functions/bounded.lean, splitting out the content about continuous functions on a compact space to topology/continuous_functions/compact.lean. Renames topology/continuous_map.lean to topology/continuous_functions/basic.lean. Renames topology/algebra/continuous_functions.lean to topology/continuous_functions/algebra.lean. Also changes the direction of the equivalences, replacing bounded_continuous_function.equiv_continuous_map_of_compact with continuous_map.equiv_bounded_of_compact (and also the more structured version). There's definitely more work to be done here, particularly giving at least some lemmas characterising the norm on C(α, β), but I wanted to do a minimal PR changing the layout first.