src/HOL/Conditionally_Complete_Lattices.thy

   then obtain a b where "\<forall>x\<in>A. a \<le> x" "\<forall>x\<in>B. b \<le> x" unfolding bdd_below_def by auto
   hence "\<forall>x \<in> A \<union> B. inf a b \<le> x" by (auto intro: Un_iff le_infI1 le_infI2)
   thus "bdd_below (A \<union> B)" unfolding bdd_below_def ..
 qed
 
-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)"
-  by (auto simp: bdd_above_def intro: le_supI1 le_supI2)
-
-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)"
-  by (auto simp: bdd_below_def intro: le_infI1 le_infI2)
+lemma bdd_above_image_sup[simp]:
+  "bdd_above ((\<lambda>x. sup (f x) (g x)) ` A) \<longleftrightarrow> bdd_above (f`A) \<and> bdd_above (g`A)"
+by (auto simp: bdd_above_def intro: le_supI1 le_supI2)
+
+lemma bdd_below_image_inf[simp]:
+  "bdd_below ((\<lambda>x. inf (f x) (g x)) ` A) \<longleftrightarrow> bdd_below (f`A) \<and> bdd_below (g`A)"
+by (auto simp: bdd_below_def intro: le_infI1 le_infI2)
+
+lemma bdd_below_UN[simp]: "finite I \<Longrightarrow> bdd_below (\<Union>i\<in>I. A i) = (\<forall>i \<in> I. bdd_below (A i))"
+by (induction I rule: finite.induct) auto
+
+lemma bdd_above_UN[simp]: "finite I \<Longrightarrow> bdd_above (\<Union>i\<in>I. A i) = (\<forall>i \<in> I. bdd_above (A i))"
+by (induction I rule: finite.induct) auto
 
 end
 
 
 text \<open>