equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 header {* Elementary topology in Euclidean space. *} |
7 header {* Elementary topology in Euclidean space. *} |
8 |
8 |
9 theory Topology_Euclidean_Space |
9 theory Topology_Euclidean_Space |
10 imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm |
10 imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith |
11 begin |
11 begin |
12 |
|
13 (* to be moved elsewhere *) |
|
14 |
|
15 lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}" |
|
16 unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner) |
|
17 by(auto simp add:power2_eq_square) |
|
18 |
|
19 lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)" |
|
20 apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)") |
|
21 apply(rule member_le_setL2) by auto |
|
22 |
12 |
23 subsection {* General notion of a topology as a value *} |
13 subsection {* General notion of a topology as a value *} |
24 |
14 |
25 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))" |
15 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))" |
26 typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" |
16 typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}" |