src/HOL/Analysis/Abstract_Topology.thy
changeset 69313 b021008c5397
parent 69286 e4d5a07fecb6
child 69325 4b6ddc5989fc
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 18 09:51:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Sun Nov 18 18:07:51 2018 +0000
     1.3 @@ -2664,11 +2664,11 @@
     1.4            (\<forall>\<U>. \<U> \<subseteq> (\<lambda>T. S \<inter> T) ` {T. closedin X T} \<longrightarrow>
     1.5             (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter>\<U> \<noteq> {})"
     1.6        by (simp add: compact_space_fip compactin_subspace closedin_subtopology image_def subset_eq Int_commute imp_conjL)
     1.7 -    also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {})"
     1.8 +    also have "\<dots> = (\<forall>\<U>\<subseteq>Collect (closedin X). (\<forall>\<F>. finite \<F> \<longrightarrow> \<F> \<subseteq> (\<inter>) S ` \<U> \<longrightarrow> \<Inter>\<F> \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {})"
     1.9        by (simp add: all_subset_image)
    1.10      also have "\<dots> = (\<forall>\<U>. (\<forall>C\<in>\<U>. closedin X C) \<and> (\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"
    1.11      proof -
    1.12 -      have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> INTER \<F> ((\<inter>) S) \<noteq> {}) \<longrightarrow> INTER \<U> ((\<inter>) S) \<noteq> {}) =
    1.13 +      have eq: "((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> \<Inter> ((\<inter>) S ` \<F>) \<noteq> {}) \<longrightarrow> \<Inter> ((\<inter>) S ` \<U>) \<noteq> {}) \<longleftrightarrow>
    1.14                  ((\<forall>\<F>. finite \<F> \<and> \<F> \<subseteq> \<U> \<longrightarrow> S \<inter> \<Inter>\<F> \<noteq> {}) \<longrightarrow> S \<inter> \<Inter>\<U> \<noteq> {})"  for \<U>
    1.15          by simp (use \<open>S \<noteq> {}\<close> in blast)
    1.16        show ?thesis