equal
deleted
inserted
replaced
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 |
10 imports |
11 SEQ |
11 Complex_Main |
12 "~~/src/HOL/Library/Diagonal_Subsequence" |
12 "~~/src/HOL/Library/Diagonal_Subsequence" |
13 "~~/src/HOL/Library/Countable_Set" |
13 "~~/src/HOL/Library/Countable_Set" |
14 Linear_Algebra |
|
15 "~~/src/HOL/Library/Glbs" |
14 "~~/src/HOL/Library/Glbs" |
16 "~~/src/HOL/Library/FuncSet" |
15 "~~/src/HOL/Library/FuncSet" |
|
16 Linear_Algebra |
17 Norm_Arith |
17 Norm_Arith |
18 begin |
18 begin |
19 |
19 |
20 lemma countable_PiE: |
20 lemma countable_PiE: |
21 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |
21 "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)" |