equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Elementary topology in Euclidean space. *} |
6 header {* Elementary topology in Euclidean space. *} |
7 |
7 |
8 theory Topology_Euclidean_Space |
8 theory Topology_Euclidean_Space |
9 imports SEQ Euclidean_Space Glbs |
9 imports SEQ Euclidean_Space "~~/src/HOL/Library/Glbs" |
10 begin |
10 begin |
11 |
11 |
12 (* to be moved elsewhere *) |
12 (* to be moved elsewhere *) |
13 |
13 |
14 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}" |
14 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}" |