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> {}"
```