# HG changeset patch
# User nipkow
# Date 1516372973 -3600
# Node ID e090941f9f422abf1a7860b1ba5b14a306fefd73
# Parent  4b921bb461f6c857f00e8527df4850c04adf7e66
moved from AFP/Gromov

diff -r 4b921bb461f6 -r e090941f9f42 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jan 19 12:14:48 2018 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jan 19 15:42:53 2018 +0100
@@ -164,11 +164,19 @@
   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_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_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_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