src/HOL/Conditionally_Complete_Lattices.thy
changeset 67458 e090941f9f42
parent 67091 1393c2340eec
child 67484 c51935a46a8f
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jan 19 12:14:48 2018 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jan 19 15:42:53 2018 +0100
     1.3 @@ -164,11 +164,19 @@
     1.4    thus "bdd_below (A \<union> B)" unfolding bdd_below_def ..
     1.5  qed
     1.6  
     1.7 -lemma bdd_above_sup[simp]: "bdd_above ((\<lambda>x. sup (f x) (g x)) ` A) \<longleftrightarrow> bdd_above (f`A) \<and> bdd_above (g`A)"
     1.8 -  by (auto simp: bdd_above_def intro: le_supI1 le_supI2)
     1.9 +lemma bdd_above_image_sup[simp]:
    1.10 +  "bdd_above ((\<lambda>x. sup (f x) (g x)) ` A) \<longleftrightarrow> bdd_above (f`A) \<and> bdd_above (g`A)"
    1.11 +by (auto simp: bdd_above_def intro: le_supI1 le_supI2)
    1.12  
    1.13 -lemma bdd_below_inf[simp]: "bdd_below ((\<lambda>x. inf (f x) (g x)) ` A) \<longleftrightarrow> bdd_below (f`A) \<and> bdd_below (g`A)"
    1.14 -  by (auto simp: bdd_below_def intro: le_infI1 le_infI2)
    1.15 +lemma bdd_below_image_inf[simp]:
    1.16 +  "bdd_below ((\<lambda>x. inf (f x) (g x)) ` A) \<longleftrightarrow> bdd_below (f`A) \<and> bdd_below (g`A)"
    1.17 +by (auto simp: bdd_below_def intro: le_infI1 le_infI2)
    1.18 +
    1.19 +lemma bdd_below_UN[simp]: "finite I \<Longrightarrow> bdd_below (\<Union>i\<in>I. A i) = (\<forall>i \<in> I. bdd_below (A i))"
    1.20 +by (induction I rule: finite.induct) auto
    1.21 +
    1.22 +lemma bdd_above_UN[simp]: "finite I \<Longrightarrow> bdd_above (\<Union>i\<in>I. A i) = (\<forall>i \<in> I. bdd_above (A i))"
    1.23 +by (induction I rule: finite.induct) auto
    1.24  
    1.25  end
    1.26