# HG changeset patch
# User nipkow
# Date 1407341023 -7200
# Node ID 84748234de9d842fe3637efd401accc260cb330b
# Parent  2e9d655054548c5cb26c4400a7292f5c680033b9
added lemma

diff -r 2e9d65505454 -r 84748234de9d src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Wed Aug 06 08:18:35 2014 +0200
+++ b/src/HOL/Lattices_Big.thy	Wed Aug 06 18:03:43 2014 +0200
@@ -633,6 +633,16 @@
 
 end
 
+lemma Max_eq_if:
+  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"
+  shows "Max A = Max B"
+proof cases
+  assume "A = {}" thus ?thesis using assms by simp
+next
+  assume "A \<noteq> {}" thus ?thesis using assms
+    by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
+qed
+
 lemma Min_antimono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"