Commit 2025-03-11 02:50 4b145864

chore(Topology/Homeomorph): split out the basic definitions (#22681) Move Homeomorph.lean to Homeomorph/Lemmas.lean, and split out a new file Homeomorph/Defs.lean which contains just the basic definitions and properties. The definitions file intentionally has very minimal imports. All declarations which require heavier imports are kept in Lemmas.lean: this can be split in future commits. Future PRs will build on this split to dissolve Homeomorph/Lemmas.lean further, such as by moving the homeomorphism about direct sums next to their construction. This is also necessary to break an import cycle in #22137. This PR gives a modest import reduction - but is a pre-requisite to more far-reaching reductions by dissolving Homeomorph/Lemmas.lean.