mathlib

832a2eb9 - refactor(topology/continuous_functions): change file layout (#6890)

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. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>