src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 52141 eff000cab70f
parent 51773 9328c6681f3c
child 52624 8a7b59a81088
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 25 15:44:08 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat May 25 15:44:29 2013 +0200
     1.3 @@ -220,7 +220,7 @@
     1.4      fix a assume "a \<in> A"
     1.5      thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
     1.6    next
     1.7 -    let ?int = "\<lambda>N. \<Inter>from_nat_into A' ` N"
     1.8 +    let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
     1.9      fix a b assume "a \<in> A" "b \<in> A"
    1.10      then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
    1.11      thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
    1.12 @@ -2617,7 +2617,7 @@
    1.13  proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
    1.14    fix A assume "compact U" and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
    1.15      and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
    1.16 -  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>uminus`A"
    1.17 +  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
    1.18      by auto
    1.19    with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
    1.20      unfolding compact_eq_heine_borel by (metis subset_image_iff)
    1.21 @@ -2627,7 +2627,7 @@
    1.22    fix A assume ?R and cover: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
    1.23    from cover have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
    1.24      by auto
    1.25 -  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>uminus`B = {}"
    1.26 +  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
    1.27      by (metis subset_image_iff)
    1.28    then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
    1.29      by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
    1.30 @@ -3041,7 +3041,7 @@
    1.31    assumes "seq_compact s"
    1.32    shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
    1.33  proof(rule, rule, rule ccontr)
    1.34 -  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k)"
    1.35 +  fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
    1.36    def x \<equiv> "helper_1 s e"
    1.37    { fix n
    1.38      have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
    1.39 @@ -4586,7 +4586,7 @@
    1.40      moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
    1.41        by (fastforce simp: subset_eq)
    1.42      ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
    1.43 -      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT)
    1.44 +      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
    1.45    qed
    1.46    then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
    1.47      and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x"