equal
deleted
inserted
replaced
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 Author: Robert Himmelmann, TU Muenchen |
3 Author: Robert Himmelmann, TU Muenchen |
4 Author: Brian Huffman, Portland State University |
4 Author: Brian Huffman, Portland State University |
5 *) |
5 *) |
6 |
6 |
7 section \<open>Elementary Topology in Euclidean Space\<close> |
7 chapter \<open>Vector Analysis\<close> |
8 |
8 |
9 theory Topology_Euclidean_Space |
9 theory Topology_Euclidean_Space |
10 imports |
10 imports |
11 Elementary_Normed_Spaces |
11 Elementary_Normed_Spaces |
12 Linear_Algebra |
12 Linear_Algebra |
13 Norm_Arith |
13 Norm_Arith |
14 begin |
14 begin |
|
15 |
|
16 section \<open>Elementary Topology in Euclidean Space\<close> |
15 |
17 |
16 lemma euclidean_dist_l2: |
18 lemma euclidean_dist_l2: |
17 fixes x y :: "'a :: euclidean_space" |
19 fixes x y :: "'a :: euclidean_space" |
18 shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis" |
20 shows "dist x y = L2_set (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis" |
19 unfolding dist_norm norm_eq_sqrt_inner L2_set_def |
21 unfolding dist_norm norm_eq_sqrt_inner L2_set_def |