equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 section%important \<open>Homeomorphism Theorems\<close> |
5 section%important \<open>Homeomorphism Theorems\<close> |
6 |
6 |
7 theory Homeomorphism |
7 theory Homeomorphism |
8 imports Path_Connected |
8 imports Homotopy |
9 begin |
9 begin |
10 |
10 |
11 lemma%unimportant homeomorphic_spheres': |
11 lemma%unimportant homeomorphic_spheres': |
12 fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" |
12 fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space" |
13 assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)" |
13 assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)" |