src/HOL/Complete_Lattices.thy
changeset 60585 48fdff264eb2
parent 60307 75e1aa7a450e
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Complete_Lattices.thy	Fri Jun 26 00:14:10 2015 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Fri Jun 26 10:20:33 2015 +0200
     1.3 @@ -1204,7 +1204,7 @@
     1.4    "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
     1.5    by (fact Sup_image_eq)
     1.6  
     1.7 -lemma Union_SetCompr_eq: "\<Union> {f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
     1.8 +lemma Union_SetCompr_eq: "\<Union>{f x| x. P x} = {a. \<exists>x. P x \<and> a \<in> f x}"
     1.9    by blast
    1.10  
    1.11  lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B x) \<longleftrightarrow> (\<exists>x\<in>A. b \<in> B x)"
    1.12 @@ -1360,7 +1360,7 @@
    1.13  lemma inj_on_UNION_chain:
    1.14    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
    1.15           INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.16 -  shows "inj_on f (\<Union> i \<in> I. A i)"
    1.17 +  shows "inj_on f (\<Union>i \<in> I. A i)"
    1.18  proof -
    1.19    {
    1.20      fix i j x y
    1.21 @@ -1390,11 +1390,11 @@
    1.22  lemma bij_betw_UNION_chain:
    1.23    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
    1.24           BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
    1.25 -  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
    1.26 +  shows "bij_betw f (\<Union>i \<in> I. A i) (\<Union>i \<in> I. A' i)"
    1.27  proof (unfold bij_betw_def, auto)
    1.28    have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.29    using BIJ bij_betw_def[of f] by auto
    1.30 -  thus "inj_on f (\<Union> i \<in> I. A i)"
    1.31 +  thus "inj_on f (\<Union>i \<in> I. A i)"
    1.32    using CH inj_on_UNION_chain[of I A f] by auto
    1.33  next
    1.34    fix i x