src/HOL/Lattices_Big.thy
changeset 57800 84748234de9d
parent 56993 e5366291d6aa
child 58467 6a3da58f7233
     1.1 --- a/src/HOL/Lattices_Big.thy	Wed Aug 06 08:18:35 2014 +0200
     1.2 +++ b/src/HOL/Lattices_Big.thy	Wed Aug 06 18:03:43 2014 +0200
     1.3 @@ -633,6 +633,16 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma Max_eq_if:
     1.8 +  assumes "finite A"  "finite B"  "\<forall>a\<in>A. \<exists>b\<in>B. a \<le> b"  "\<forall>b\<in>B. \<exists>a\<in>A. b \<le> a"
     1.9 +  shows "Max A = Max B"
    1.10 +proof cases
    1.11 +  assume "A = {}" thus ?thesis using assms by simp
    1.12 +next
    1.13 +  assume "A \<noteq> {}" thus ?thesis using assms
    1.14 +    by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
    1.15 +qed
    1.16 +
    1.17  lemma Min_antimono:
    1.18    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
    1.19    shows "Min N \<le> Min M"