src/HOL/Lattices_Big.thy
changeset 66425 8756322dc5de
parent 66364 fa3247e6ee4b
child 67036 783c901a62cb
     1.1 --- a/src/HOL/Lattices_Big.thy	Mon Aug 14 21:42:55 2017 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Tue Aug 15 09:29:35 2017 +0200
     1.3 @@ -580,6 +580,22 @@
     1.4    from assms show "x \<le> Max A" by simp
     1.5  qed
     1.6  
     1.7 +lemma eq_Min_iff:
     1.8 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
     1.9 +by (meson Min_in Min_le antisym)
    1.10 +
    1.11 +lemma Min_eq_iff:
    1.12 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
    1.13 +by (meson Min_in Min_le antisym)
    1.14 +
    1.15 +lemma eq_Max_iff:
    1.16 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
    1.17 +by (meson Max_in Max_ge antisym)
    1.18 +
    1.19 +lemma Max_eq_iff:
    1.20 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
    1.21 +by (meson Max_in Max_ge antisym)
    1.22 +
    1.23  context
    1.24    fixes A :: "'a set"
    1.25    assumes fin_nonempty: "finite A" "A \<noteq> {}"