proposed reorg

Stream: general

[Scott Morrison]

@Heather Macbeth, @Sebastien Gouezel,

I am thinking about replacing

• topology/bounded_continuous_function.lean
• topology/continuous_map.lean
• topology/algebra/continuous_functions.lean

with

• topology/continuous_functions/basic.lean
• topology/continuous_functions/bounded.lean
• topology/continuous_functions/compact.lean

[Scott Morrison]

where basic.lean will contain the current continuous_map.lean, and much of algebra/continuous_functions, and bounded.lean will contain the current bounded_continuous_function.lean, except that I will move all the constructions of normed gadgets on C(X, Y) in compact.lean, which depends on both basic and bounded.

[Scott Morrison]

The rationale is basically that even though I transported various structure from bounded continuous functions to "all" continuous functions when the domain is compact in #6701, the file structure is basically a dead-end now. It's very inconvenient to add lemmas about normed gadgets on C(X,Y), while inside the bounded_continuous_functions.lean file.

[Scott Morrison]

I think my proposed layout would also make it straightforward to add continuous_functions/vanishing_at_infty.lean when the time comes.

[Sebastien Gouezel]

Sounds good to me!