equal
deleted
inserted
replaced
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)" |
22 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
22 by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) |
23 |
|
24 lemma countable_rat: "countable \<rat>" |
|
25 unfolding Rats_def by auto |
|
26 |
23 |
27 subsection {* Topological Basis *} |
24 subsection {* Topological Basis *} |
28 |
25 |
29 context topological_space |
26 context topological_space |
30 begin |
27 begin |