src/HOL/Conditionally_Complete_Lattices.thy
changeset 62379 340738057c8c
parent 62343 24106dc44def
child 62626 de25474ce728
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Feb 19 13:40:50 2016 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon Feb 22 14:37:56 2016 +0000
     1.3 @@ -646,4 +646,44 @@
     1.4  apply (metis eq cSUP_upper)
     1.5  done 
     1.6  
     1.7 +lemma cSUP_UNION:
     1.8 +  fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
     1.9 +  assumes ne: "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> B(x) \<noteq> {}"
    1.10 +      and bdd_UN: "bdd_above (\<Union>x\<in>A. f ` B x)"
    1.11 +  shows "(SUP z : \<Union>x\<in>A. B x. f z) = (SUP x:A. SUP z:B x. f z)"
    1.12 +proof -
    1.13 +  have bdd: "\<And>x. x \<in> A \<Longrightarrow> bdd_above (f ` B x)"
    1.14 +    using bdd_UN by (meson UN_upper bdd_above_mono)
    1.15 +  obtain M where "\<And>x y. x \<in> A \<Longrightarrow> y \<in> B(x) \<Longrightarrow> f y \<le> M"
    1.16 +    using bdd_UN by (auto simp: bdd_above_def)
    1.17 +  then have bdd2: "bdd_above ((\<lambda>x. SUP z:B x. f z) ` A)"
    1.18 +    unfolding bdd_above_def by (force simp: bdd cSUP_le_iff ne(2))
    1.19 +  have "(SUP z:\<Union>x\<in>A. B x. f z) \<le> (SUP x:A. SUP z:B x. f z)"
    1.20 +    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper2 simp: bdd2 bdd)
    1.21 +  moreover have "(SUP x:A. SUP z:B x. f z) \<le> (SUP z:\<Union>x\<in>A. B x. f z)"
    1.22 +    using assms by (fastforce simp add: intro!: cSUP_least intro: cSUP_upper simp: image_UN bdd_UN)
    1.23 +  ultimately show ?thesis
    1.24 +    by (rule order_antisym)
    1.25 +qed
    1.26 +
    1.27 +lemma cINF_UNION:
    1.28 +  fixes f :: "_ \<Rightarrow> 'b::conditionally_complete_lattice"
    1.29 +  assumes ne: "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> B(x) \<noteq> {}"
    1.30 +      and bdd_UN: "bdd_below (\<Union>x\<in>A. f ` B x)"
    1.31 +  shows "(INF z : \<Union>x\<in>A. B x. f z) = (INF x:A. INF z:B x. f z)"
    1.32 +proof -
    1.33 +  have bdd: "\<And>x. x \<in> A \<Longrightarrow> bdd_below (f ` B x)"
    1.34 +    using bdd_UN by (meson UN_upper bdd_below_mono)
    1.35 +  obtain M where "\<And>x y. x \<in> A \<Longrightarrow> y \<in> B(x) \<Longrightarrow> f y \<ge> M"
    1.36 +    using bdd_UN by (auto simp: bdd_below_def)
    1.37 +  then have bdd2: "bdd_below ((\<lambda>x. INF z:B x. f z) ` A)"
    1.38 +    unfolding bdd_below_def by (force simp: bdd le_cINF_iff ne(2))
    1.39 +  have "(INF z:\<Union>x\<in>A. B x. f z) \<le> (INF x:A. INF z:B x. f z)"
    1.40 +    using assms by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower simp: bdd2 bdd)
    1.41 +  moreover have "(INF x:A. INF z:B x. f z) \<le> (INF z:\<Union>x\<in>A. B x. f z)"
    1.42 +    using assms  by (fastforce simp add: intro!: cINF_greatest intro: cINF_lower2  simp: bdd bdd_UN bdd2)
    1.43 +  ultimately show ?thesis
    1.44 +    by (rule order_antisym)
    1.45 +qed
    1.46 +
    1.47  end