29 |
29 |
30 lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)" |
30 lemma open_Un [intro]: "open S \<Longrightarrow> open T \<Longrightarrow> open (S \<union> T)" |
31 using open_Union [of "{S, T}"] by simp |
31 using open_Union [of "{S, T}"] by simp |
32 |
32 |
33 lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)" |
33 lemma open_UN [intro]: "\<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Union>x\<in>A. B x)" |
34 unfolding SUP_def by (rule open_Union) auto |
34 using open_Union [of "B ` A"] by simp |
35 |
35 |
36 lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)" |
36 lemma open_Inter [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. open T \<Longrightarrow> open (\<Inter>S)" |
37 by (induct set: finite) auto |
37 by (induct set: finite) auto |
38 |
38 |
39 lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)" |
39 lemma open_INT [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. open (B x) \<Longrightarrow> open (\<Inter>x\<in>A. B x)" |
40 unfolding INF_def by (rule open_Inter) auto |
40 using open_Inter [of "B ` A"] by simp |
41 |
41 |
42 lemma openI: |
42 lemma openI: |
43 assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S" |
43 assumes "\<And>x. x \<in> S \<Longrightarrow> \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S" |
44 shows "open S" |
44 shows "open S" |
45 proof - |
45 proof - |
68 |
68 |
69 lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)" |
69 lemma closed_Union [intro]: "finite S \<Longrightarrow> \<forall>T\<in>S. closed T \<Longrightarrow> closed (\<Union>S)" |
70 by (induct set: finite) auto |
70 by (induct set: finite) auto |
71 |
71 |
72 lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)" |
72 lemma closed_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. closed (B x) \<Longrightarrow> closed (\<Union>x\<in>A. B x)" |
73 unfolding SUP_def by (rule closed_Union) auto |
73 using closed_Union [of "B ` A"] by simp |
74 |
74 |
75 lemma open_closed: "open S \<longleftrightarrow> closed (- S)" |
75 lemma open_closed: "open S \<longleftrightarrow> closed (- S)" |
76 unfolding closed_def by simp |
76 unfolding closed_def by simp |
77 |
77 |
78 lemma closed_open: "closed S \<longleftrightarrow> open (- S)" |
78 lemma closed_open: "closed S \<longleftrightarrow> open (- S)" |
167 |
167 |
168 hide_fact (open) UNIV Int UN Basis |
168 hide_fact (open) UNIV Int UN Basis |
169 |
169 |
170 lemma generate_topology_Union: |
170 lemma generate_topology_Union: |
171 "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)" |
171 "(\<And>k. k \<in> I \<Longrightarrow> generate_topology S (K k)) \<Longrightarrow> generate_topology S (\<Union>k\<in>I. K k)" |
172 unfolding SUP_def by (intro generate_topology.UN) auto |
172 using generate_topology.UN [of "K ` I"] by auto |
173 |
173 |
174 lemma topological_space_generate_topology: |
174 lemma topological_space_generate_topology: |
175 "class.topological_space (generate_topology S)" |
175 "class.topological_space (generate_topology S)" |
176 by default (auto intro: generate_topology.intros) |
176 by default (auto intro: generate_topology.intros) |
177 |
177 |
1950 "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow> |
1950 "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow> |
1951 s \<inter> (\<Inter> f) \<noteq> {}" |
1951 s \<inter> (\<Inter> f) \<noteq> {}" |
1952 unfolding compact_fip by auto |
1952 unfolding compact_fip by auto |
1953 |
1953 |
1954 lemma compact_imp_fip_image: |
1954 lemma compact_imp_fip_image: |
1955 "compact s \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> closed (f i)) \<Longrightarrow> (\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})) \<Longrightarrow> |
1955 assumes "compact s" |
1956 s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}" |
1956 and P: "\<And>i. i \<in> I \<Longrightarrow> closed (f i)" |
1957 using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def |
1957 and Q: "\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})" |
1958 by (metis image_iff) |
1958 shows "s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}" |
|
1959 proof - |
|
1960 note `compact s` |
|
1961 moreover from P have "\<forall>i \<in> f ` I. closed i" by blast |
|
1962 moreover have "\<forall>A. finite A \<and> A \<subseteq> f ` I \<longrightarrow> (s \<inter> (\<Inter>A) \<noteq> {})" |
|
1963 proof (rule, rule, erule conjE) |
|
1964 fix A :: "'a set set" |
|
1965 assume "finite A" |
|
1966 moreover assume "A \<subseteq> f ` I" |
|
1967 ultimately obtain B where "B \<subseteq> I" and "finite B" and "A = f ` B" |
|
1968 using finite_subset_image [of A f I] by blast |
|
1969 with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}" by simp |
|
1970 qed |
|
1971 ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}" by (rule compact_imp_fip) |
|
1972 then show ?thesis by simp |
|
1973 qed |
1959 |
1974 |
1960 end |
1975 end |
1961 |
1976 |
1962 lemma (in t2_space) compact_imp_closed: |
1977 lemma (in t2_space) compact_imp_closed: |
1963 assumes "compact s" shows "closed s" |
1978 assumes "compact s" shows "closed s" |