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\<close> |
7 chapter \<open>Topology\<close> |
8 |
8 |
9 theory Elementary_Topology |
9 theory Elementary_Topology |
10 imports |
10 imports |
11 "HOL-Library.Set_Idioms" |
11 "HOL-Library.Set_Idioms" |
12 "HOL-Library.Disjoint_Sets" |
12 "HOL-Library.Disjoint_Sets" |
13 Product_Vector |
13 Product_Vector |
14 begin |
14 begin |
15 |
15 |
|
16 |
|
17 section \<open>Elementary Topology\<close> |
16 |
18 |
17 subsection \<open>TODO: move?\<close> |
19 subsection \<open>TODO: move?\<close> |
18 |
20 |
19 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" |
21 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)" |
20 using openI by auto |
22 using openI by auto |