src/HOL/Conditionally_Complete_Lattices.thy
changeset 54261 89991ef58448
parent 54259 71c701dc5bf9
child 54262 326fd7103cb4
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:44:59 2013 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
     1.3 @@ -90,6 +90,12 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma (in order_top) bdd_above_top[simp, intro!]: "bdd_above A"
     1.8 +  by (rule bdd_aboveI[of _ top]) simp
     1.9 +
    1.10 +lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
    1.11 +  by (rule bdd_belowI[of _ bot]) simp
    1.12 +
    1.13  context lattice
    1.14  begin
    1.15  
    1.16 @@ -270,6 +276,12 @@
    1.17  lemma cSUP_upper2: "bdd_above (f ` A) \<Longrightarrow> x \<in> A \<Longrightarrow> u \<le> f x \<Longrightarrow> u \<le> SUPR A f"
    1.18    by (auto intro: cSUP_upper assms order_trans)
    1.19  
    1.20 +lemma cSUP_const: "A \<noteq> {} \<Longrightarrow> (SUP x:A. c) = c"
    1.21 +  by (intro antisym cSUP_least) (auto intro: cSUP_upper)
    1.22 +
    1.23 +lemma cINF_const: "A \<noteq> {} \<Longrightarrow> (INF x:A. c) = c"
    1.24 +  by (intro antisym cINF_greatest) (auto intro: cINF_lower)
    1.25 +
    1.26  lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> INFI A f \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
    1.27    by (metis cINF_greatest cINF_lower assms order_trans)
    1.28